AI helps you reading Science
AI generates interpretation videos
AI extracts and analyses the key points of the paper to generate videos automatically
AI parses the academic lineage of this thesis
AI extracts a summary of this paper
Implementation, and usage of an interpreter for algebraic specifications that is seamlessly integrated with Java
A Tool for Writing and Debugging Algebraic Specifications
ICSE, pp.449-458, (2004)
Despite their benefits, programmers rarely use formalspecifications, because they are difficult to write and theyrequire an up front investment in time. To address these issues,we present a tool that helps programmers write anddebug algebraic specifications. Given an algebraic specification, our tool instantiates a prototype that can be u...More
PPT (Upload PPT)
- Formal specifications have many software engineering benefits. Perhaps the most important advantage of formal specifications is that they can provide an unambiguous and possibly machine checkable documentation of an interface.
- The authors' tool interprets algebraic specifications using term rewriting, which is a well studied area [6, 20].
- The authors' system is preinitialized with axioms pertaining to intAdd. The authors' approach provides a seamless integration between an interpreter for algebraic specifications and Java applications.
- Formal specifications have many software engineering benefits
- We demonstrate the applicability of our tools for the scenario shown in Figure 1 in a case study (Section 5.2)
- Similar to what we describe in Section 5.1, debugging the discovered specification is an iterative process consisting of three steps: (i) using the specification interpreter to run the client application, (ii) understanding the debugging output, (iii) adding new algebraic axioms to the specification or modifying the existing axioms
- By using the specification interpreter, we focused on the axioms needed for a particular run of our client application
-  we described a system that can discover algebraic specifications automatically from Java classes
- Implementation, and usage of an interpreter for algebraic specifications that is seamlessly integrated with Java
- If a programmer wants to use a specification for a LinkedList, the simulation set would contain only LinkedList, and the algebraic specification would specify the behavior of LinkedList.
- In addition to the algebraic specifications and the simulation set, users of the system provide a client that uses the classes in the simulation set.
- The interpreter (i) reduces the size of the terms that model the state of an object (ii) computes the return value of the simulated Java methods.
- As an example for (i), the interpreter uses the axiom forall o:Object add(NewLinkedList().state,o).state (Axiom 4) == addFirst(LinkedList().state,o).state to transform the algebraic term Term 1 into addAll(NewLinkedList().state,addFirst(
- Section 3 illustrated how the authors use rewriting to interpret algebraic specifications.
- Rewriting interprets the axioms in the algebraic specification as rewriting rules that transform one term into another.
- Using the axioms for the contains operation, the algebraic interpreter will reduce this relation by rewriting it to true==true.
- Term = add(NewHashSet().state,Integer@1776).retval Client.java, line 6: Algebraic Interpreter failed to compute a value.
- Note that this is inadequate in general since it does not say anything about adding to a non-empty HashSet. The second axiom says that immediately after adding an object to the HashSet, invoking contains(add(h,o).state,o).retval returns true.
- On running the modified client and specification set, the system gives the following error message: test 0 = true Client.java, line 6: Algebraic Interpreter failed to compute a value.
- The authors used the specification discovery tool  to generate a specification for the java.util.ArrayList class contained in Sun’s Java Development Kit. The authors used the algebraic interpreter to debug the discovered specification.
- Similar to what the authors describe in Section 5.1, debugging the discovered specification is an iterative process consisting of three steps: (i) using the specification interpreter to run the client application, (ii) understanding the debugging output, (iii) adding new algebraic axioms to the specification or modifying the existing axioms.
- The discovery tool currently cannot find these 5 axioms because the state of the Iterator object is modeled as the return value of the operation iterator() of another class (ArrayList).
- The authors illustrate the usefulness of this approach by giving case studies and by presenting performance results for the prototype produced by the tool
- Previously  we described a system that can discover algebraic specifications automatically from Java classes. The output of that system can be used as a starting point for developing a specification of an existing Java class. The current paper and our previous paper share the goal of making formal specification techniques more appealing for practical use. Both techniques use the same specification language and are designed to be used together.
There is a vast body of prior work on term rewriting systems [6, 20]. Prior work has also studied the idea of using term rewriting to simulate a software component. For example, Wang and Parnas proposed the trace rewriting method to simulate software modules . However, they focus on the rewriting technique for their system and unlike us, do not integrate their system into a programming language or provide details of an implementation. Implementations of other rewriting engines and rewriting language have been used to provide prototyping [10, 7, 20], but again, to our knowledge, they do not interact with a client written in a modern programming language. Thus, these systems do not provide the software engineering benefits that our approach offers. Antoy and Hamlet  propose self-checking ADTs, which integrate rewriting into C++ and Java classes. Among other details, our system differs by (i) fully automating the integration of Java code and the algebraic interpreter with a custom class loader, and (ii) a more expressive algebraic specification language that has been customized for being embedded into Java (e.g., we allow operations to both modify the state of an object and return a value). Antoy and Hamlet manually implement representation mappings as C++/Java functions to allow intensional comparisons, which might be a useful addition to our current system.
- ∗ This work is supported by NSF grants CCR-0085792, CCR-0133457, and CCR-0086255
- G. Ammons, R. Bodik, and J. R. Larus. Mining specifications. In Proceedings of the 29th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pages 4–16, 2002.
- S. Antoy and D. Hamlet. Automatically checking an implementation against its formal specification. IEEE Transactions on Software Engineering, 26(1), Jan. 2000.
- Apache Software Foundation. BCEL—byte code engineering library. http://jakarta.apache.org/bcel/.
- H. Y. Chen, T. H. Tse, F. T. Chan, and T. Y. Chen. In black and white: An integrated approach to class-level testing of object oriented programs. ACM Transactions on Software Engineering, 7(3), July 1998.
- H. Y. Chen, T. H. Tse, and T. Y. Chen. TACCLE: A methodology for object-oriented software testing at the class and cluster levels. ACM Transactions on Software Engineering, 10(4):56–109, Jan. 2001.
- N. Dershowitz and D. A. Plaisted. Handbook of Automated Reasoning, volume 1, chapter Rewriting. Elsevier, 2001.
- N. Dershowitz and L. Vigneron. Database of rewriting systems. http://www.loria.fr/vigneron/RewritingHP/systems.html, 2003.
- R. Doong and P. G. Frankl. The ASTOOT approach to testing object-oriented programs. ACM Transactions on Software Engineering, 3(2), Apr. 1994.
- M. D. Ernst, J. Cockrell, W. G. Griswold, and D. Notkin. Dynamically discovering likely program invariants to support program evolution. ACM Transactions on Software Engineering, 27(2):1–25, Feb. 2001.
- http://www.ldl.jaist.ac.jp/cafeobj/, 2003.
- J. Gannon, P. McMullin, and R. Hamlet. Data-abstraction implementation, specification and testing. ACM Transactions on Programming Languages and Systems, 3(3):211–
- D. Gries. The science of programming. Texts and monographs in computer science. Springer-Verlag, 1981.
- J. V. Guttag and J. J. Horning. The algebraic specification of abstract data types. Acta Informatica, 10:27–52, 1978.
- J. Henkel and A. Diwan. Discovering algebraic specifications from Java classes. In L. Cardelli, editor, ECOOP 2003 - Object-Oriented Programming, 17th European Conference, Darmstadt, July 2003. Springer.
- J. Henkel and A. Diwan. Case study: Debugging a discovered specification for java.util.arraylist by using algebraic interpretation. Technical Report CU-CS-970-04, University of Colorado at Boulder, 2004.
- M. Hughes and D. Stotts. Daistish: Systematic algebraic testing for OO programs in the presence of side-effects. In Proceedings of the International Symposium on Software Testing and Verification, San Diego, California, 1996. MIT Press, 1996.
-  J. W. Nimmer and M. D. Ernst. Static verification of dynamically detected program invariants: Integrating daikon and esc/java. In Proceedings of RV’01, First Workshop on Runtime Verification, Paris, France, July 2001.
-  S. Sankar. Run-time consistency checking of algebraic specifications. In Proceedings of the Symposium on Testing, Analysis, and Verification, Victoria, British Columbia, Canada, Sept. 1991.
-  TeReSe. Term Rewriting Systems, volume 55 of Cambridge Tracts in Theoretical Computer Science. Cambridge University Press, 2003.
-  J. W. Thatcher, E. G. Wagner, and J. B. Wright. Data type specification: Parameterization and the power of specification techniques. ACM Transactions on Programming Languages and Systems, 4(4), Oct. 1982.
-  R. Vallee-Rai, E. Gagnon, L. J. Hendren, P. Lam, P. Pominville, and V. Sundaresan. Optimizing Java bytecode using the Soot framework: Is it feasible? In Compiler Construction, 9th International Conference (CC 2000), pages 18–34, 2000.
-  Y. Wang and D. L. Parnas. Simulating the behavior of software modules by trace rewriting. ACM Transactions on Software Engineering, 20(10), Oct. 1994.