- Author:
- J. M. Wing
Current research in specifications is beginning to emphasize the practical use of formal specifications in program design. This thesis presents a specification approach, a specification language that supports that approach, and some ways to evaluate specifications written in that language. The two-tiered approach separates the specification of underlying abstractions from the specification of state transformations. In this approach, state transformations and target programming language dependencies are isolated into an interface language component. All interface specifications are built upon shared language specifications that describe the underlying abstractions. This thesis presents an interface specification language for the CLU programming language and presumes the use of the Larch shared language. This thesis also suggests a number of kinds of analyses that one might want to perform on two-tiered specifications. These are related to the consistency, completeness, and strength of specifications, and are all presented in terms of the theories associated with specifications.
Cited By
Bao Y, Leavens G and Ernst G Conditional effects in fine-grained region logic Proceedings of the 17th Workshop on Formal Techniques for Java-like Programs, (1-6)- Flanagan C, Leino K, Lillibridge M, Nelson G, Saxe J and Stata R (2013). PLDI 2002, ACM SIGPLAN Notices, 48:4S, (22-33), Online publication date: 9-Jul-2013.
- Leavens G and Muller P Information Hiding and Visibility in Interface Specifications Proceedings of the 29th international conference on Software Engineering, (385-395)
- Chalin P A Sound Assertion Semantics for the Dependable Systems Evolution Verifying Compiler Proceedings of the 29th international conference on Software Engineering, (23-33)
- Leavens G, Baker A and Ruby C (2006). Preliminary design of JML, ACM SIGSOFT Software Engineering Notes, 31:3, (1-38), Online publication date: 1-May-2006.
- Leavens G JML’s rich, inherited specifications for behavioral subtypes Proceedings of the 8th international conference on Formal Methods and Software Engineering, (2-34)
- Leavens G, Cheon Y, Clifton C, Ruby C and Cok D (2005). How the design of JML accommodates both runtime assertion checking and formal verification, Science of Computer Programming, 55:1-3, (185-208), Online publication date: 1-Mar-2005.
- Flanagan C, Leino K, Lillibridge M, Nelson G, Saxe J and Stata R Extended static checking for Java Proceedings of the ACM SIGPLAN 2002 conference on Programming language design and implementation, (234-245)
- Flanagan C, Leino K, Lillibridge M, Nelson G, Saxe J and Stata R (2002). Extended static checking for Java, ACM SIGPLAN Notices, 37:5, (234-245), Online publication date: 17-May-2002.
- Hamie A Enhancing the Object Constraint Language for More Expressive Specifications Proceedings of the Sixth Asia Pacific Software Engineering Conference
- Wang C and Musser D (1997). Dynamic Verification of C++ Generic Algorithms, IEEE Transactions on Software Engineering, 23:5, (314-323), Online publication date: 1-May-1997.
- Tan Y Interface language for supporting programming styles Proceedings of the Workshop on Interface Definition Languages, (74-83)
- Leavens G Inheritance of interface specifications (extended abstract) Proceedings of the Workshop on Interface Definition Languages, (129-138)
- Tan Y (1994). Interface language for supporting programming styles, ACM SIGPLAN Notices, 29:8, (74-83), Online publication date: 1-Aug-1994.
- Leavens G (1994). Inheritance of interface specifications (extended abstract), ACM SIGPLAN Notices, 29:8, (129-138), Online publication date: 1-Aug-1994.
- Vandevoorde M and Guttag J Using specialized procedures and specification-based analysis to reduce the runtime costs of modularity Proceedings of the 2nd ACM SIGSOFT symposium on Foundations of software engineering, (121-127)
- Vandevoorde M and Guttag J (1994). Using specialized procedures and specification-based analysis to reduce the runtime costs of modularity, ACM SIGSOFT Software Engineering Notes, 19:5, (121-127), Online publication date: 1-Dec-1994.
- Leavens G and Weihl W Reasoning about object-oriented programs that use subtypes Proceedings of the European conference on object-oriented programming on Object-oriented programming systems, languages, and applications, (212-223)
- Leavens G and Weihl W (1990). Reasoning about object-oriented programs that use subtypes, ACM SIGPLAN Notices, 25:10, (212-223), Online publication date: 1-Oct-1990.
- Herlihy M and Wing J Specifying graceful degradation in distributed systems Proceedings of the sixth annual ACM Symposium on Principles of distributed computing, (167-177)
Recommendations
Design and Implementation of a Tool for Specifying Specification in SOFL
Revised Selected Papers of the Second International Workshop on Structured Object-Oriented Formal Language and Method - Volume 7787Structure Object-oriented Formal Language SOFL is not just a formal language for writing formal specification. It is also an approach and a methodology. SOFL provides a three-step approach for modelling a software system using formal specification. ...
Specifying generic Java programs: two case studies
LDTA '10: Proceedings of the Tenth Workshop on Language Descriptions, Tools and ApplicationsThis work investigates the question of modular specification of generic Java classes and methods. We propose extensions to the Krakatoa Modeling Language, a part of the Why platform for proving that a Java or C program is a correct implementation of ...