AI helps you reading Science

AI generates interpretation videos

AI extracts and analyses the key points of the paper to generate videos automatically


pub
Go Generating

AI Traceability

AI parses the academic lineage of this thesis


Master Reading Tree
Generate MRT

AI Insight

AI extracts a summary of this paper


Weibo:
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)

Cited: 54|Views137
EI

Abstract

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

Code:

Data:

0
Introduction
  • 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.
Highlights
  • 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
  • [14] 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
Results
  • 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 [14] 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.
Conclusion
  • 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
Related work
  • Previously [14] 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 [23]. 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 [2] 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.
Funding
  • ∗ This work is supported by NSF grants CCR-0085792, CCR-0133457, and CCR-0086255
Reference
  • 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.
    Google ScholarLocate open access versionFindings
  • S. Antoy and D. Hamlet. Automatically checking an implementation against its formal specification. IEEE Transactions on Software Engineering, 26(1), Jan. 2000.
    Google ScholarLocate open access versionFindings
  • Apache Software Foundation. BCEL—byte code engineering library. http://jakarta.apache.org/bcel/.
    Findings
  • 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.
    Google ScholarLocate open access versionFindings
  • 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.
    Google ScholarLocate open access versionFindings
  • N. Dershowitz and D. A. Plaisted. Handbook of Automated Reasoning, volume 1, chapter Rewriting. Elsevier, 2001.
    Google ScholarLocate open access versionFindings
  • N. Dershowitz and L. Vigneron. Database of rewriting systems. http://www.loria.fr/vigneron/RewritingHP/systems.html, 2003.
    Findings
  • R. Doong and P. G. Frankl. The ASTOOT approach to testing object-oriented programs. ACM Transactions on Software Engineering, 3(2), Apr. 1994.
    Google ScholarLocate open access versionFindings
  • 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.
    Google ScholarLocate open access versionFindings
  • http://www.ldl.jaist.ac.jp/cafeobj/, 2003.
    Findings
  • J. Gannon, P. McMullin, and R. Hamlet. Data-abstraction implementation, specification and testing. ACM Transactions on Programming Languages and Systems, 3(3):211–
    Google ScholarLocate open access versionFindings
  • D. Gries. The science of programming. Texts and monographs in computer science. Springer-Verlag, 1981.
    Google ScholarFindings
  • J. V. Guttag and J. J. Horning. The algebraic specification of abstract data types. Acta Informatica, 10:27–52, 1978.
    Google ScholarLocate open access versionFindings
  • 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.
    Google ScholarLocate open access versionFindings
  • 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.
    Google ScholarFindings
  • 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.
    Google ScholarLocate open access versionFindings
  • [18] 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.
    Google ScholarLocate open access versionFindings
  • [19] 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.
    Google ScholarLocate open access versionFindings
  • [20] TeReSe. Term Rewriting Systems, volume 55 of Cambridge Tracts in Theoretical Computer Science. Cambridge University Press, 2003.
    Google ScholarFindings
  • [21] 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.
    Google ScholarLocate open access versionFindings
  • [22] 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.
    Google ScholarLocate open access versionFindings
  • [23] Y. Wang and D. L. Parnas. Simulating the behavior of software modules by trace rewriting. ACM Transactions on Software Engineering, 20(10), Oct. 1994.
    Google ScholarLocate open access versionFindings
0
Your rating :

No Ratings

Tags
Comments
数据免责声明
页面数据均来自互联网公开来源、合作出版商和通过AI技术自动分析结果,我们不对页面数据的有效性、准确性、正确性、可靠性、完整性和及时性做出任何承诺和保证。若有疑问,可以通过电子邮件方式联系我们:report@aminer.cn