Manuel Fähndrich
Michael Barnett
ABSTRACT
Specifying application interfaces (APIs) with information that goes beyond method argument and return types is a long-standing quest of programming language researchers and practitioners. The number of type system extensions or specification languages is a testament to that. Unfortunately, the number of such systems is also roughly equal to the number of tools that consume them. In other words, every tool comes with its own specification language.
In this paper we argue that for modern object-oriented languages, using an embedding of contracts as code is a better approach. We exemplify our embedding of Code Contracts on the Microsoft managed execution platform (.NET) using the C# programming language. The embedding works as well in Visual Basic. We discuss the numerous advantages of our approach and the technical challenges, as well as the status of tools that consume the embedded contracts.
- Thomas Ball, Byron Cook, Vladimir Levin, and Sriram K. Rajamani. SLAM and static driver verifier: Technology transfer of formal methods inside Microsoft. In Integrated Formal Methods, pages 1--20. Springer, 2004.Google Scholar
Cross Ref
- Mike Barnett, K. Rustan M. Leino, and Wolfram Schulte. The Spec# programming system: An overview. In CASSIS, volume 3362 of LNCS. Springer, 2004. Google ScholarDigital Library
- Bernard Carré and Jonathan Garnsworthy. SPARK---an annotated Ada subset for safety-critical programming. In TRI-Ada '90: Proceedings of the conference on TRI-ADA '90, pages 392--402. ACM, 1990. Google ScholarDigital Library
- Markus Dahlweid, Michal Moskal, Thomas Santen, Stephan Tobies, and Wolfram Schulte. VCC: Contract-based modular verification of concurrent C. In 31st International Conference on Software Engineering, ICSE 2009, May 16--24, 2009, Vancouver, Canada, Companion Volume, pages 429--430. IEEE, 2009.Google ScholarCross Ref
- Manuvir Das. Formal specifications on industrial-strength code-from myth to reality. In Computer Aided Verification, 18th International Conference, CAV 2006, page 1, 2006. Google ScholarDigital Library
- Robert Deline and Manuel Fahndrich. Typestates for objects. In Proceedings of the 18th European Conference on Object-Oriented Programming, pages 465--490. Springer, 2004.Google ScholarCross Ref
- Manuel Fähndrich and K. Rustan M. Leino. Declaring and checking non-null types in an object-oriented language. In OOPSLA '03: Proceedings of the 18th annual ACM SIGPLAN conference on Object-oriented programing, systems, languages, and applications, pages 302--312. ACM, 2003. Google ScholarDigital Library
- Patrice Godefroid. Compositional dynamic test generation. In Proceedings of the 34th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, pages 47--54, 2007. Google ScholarDigital Library
- Neelam Gupta, Aditya P. Mathur, and Mary Lou Soffa. Generating test data for branch coverage. In ASE: IEEE International Conference on Automated Software Engineering, pages 219--228, 2000. Google ScholarDigital Library
- James C. King. Symbolic execution and program testing. Communications of the ACM, 19(7):385--394, 1976. Google ScholarDigital Library
- Bogdan Korel. Automated software test data generation. IEEE Transactions on Software Engineering, 16(8):870--879, 1990. Google ScholarDigital Library
- Gary T. Leavens, Albert L. Baker, and Clyde Ruby. Preliminary design of JML: A behavioral interface specification language for Java. SIGSOFT, 31(3):1--38, March 2006. Google ScholarDigital Library
- K. Rustan M. Leino. Data groups: specifying the modification of extended state. In OOPSLA '98: Proceedings of the 13th ACM SIGPLAN conference on Object-oriented programming, systems, languages, and applications, pages 144--153, 1998. Google ScholarDigital Library
- F. Logozzo and M. A. Fähndrich. On the relative completeness of bytecode analysis versus source code analysis. In CC'08, LNCS. Springer-Verlag, March 2008. Google ScholarDigital Library
- F. Logozzo and M. A. Fähndrich. Pentagons: A weakly relational abstract domain for the efficient validation of array accesses. In ACM SAC'08 - OOPS. ACM Press, March 2008. Google ScholarDigital Library
- B. Meyer. Eiffel: The Language. Prentice Hall, 1992. Google ScholarDigital Library
- Matthew M. Papi, Mahmood Ali, Telmo Luis Correa, Jr., Jeff H. Perkins, and Michael D. Ernst. Practical pluggable types for Java. In ISSTA '08: Proceedings of the 2008 international symposium on Software testing and analysis, pages 201--212. ACM, 2008. Google ScholarDigital Library
- Nikolai Tillmann and Jonathan de Halleux. Pex-white box test generation for .NET. In TAP: Tests and Proofs Second International Conference, pages 134--153, 2008. Google ScholarDigital Library
- Hongwei Xi and Frank Pfenning. Dependent types in practical programming. In POPL '99: Proceedings of the 26th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, pages 214--227. ACM, 1999. Google ScholarDigital Library
- Dana N. Xu, Simon L. Peyton Jones, and Koen Claessen. Static contract checking for Haskell. In Proceedings of the 36th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pages 41--52. ACM, 2009. Google ScholarDigital Library
Index Terms
- Embedded contract languages
Recommendations
P#: a concurrent prolog for the .NET framework
We discuss P#, our implementation of a tool that allows interoperation between a concurrent superset of the Prolog programming language and C#. This enables Prolog to be used as a native implementation language for Microsoft's .NET platform. P# compiles ...
Traditional and more "exotic" .NET languages: VB .NET, J#, C# and SML .NET
We study the .NET platform, various .NET languages and their interoperability (with an emphasis on C# and SML .NET), compare C# and Java 1.5, and develop related educational material to be used in a Programming Paradigms course. Introducing .NET - one ...
Essential ASP.NET2
A review of Essential ASP.NET with Examples in C# and Essential ASP.NET with Examples in Visual Basic .NET by Fritz Onion.
Comments