Skip to main content
SpringerLink
Log in

The Spec# Programming System: An Overview

  • Conference paper
Construction and Analysis of Safe, Secure, and Interoperable Smart Devices (CASSIS 2004)

Part of the book series: Lecture Notes in Computer Science ((LNSC,volume 3362))

Abstract

The Spec# programming system is a new attempt at a more cost effective way to develop and maintain high-quality software. This paper describes the goals and architecture of the Spec# programming system, consisting of the object-oriented Spec# programming language, the Spec# compiler, and the Boogie static program verifier. The language includes constructs for writing specifications that capture programmer intentions about how methods and data are to be used, the compiler emits run-time checks to enforce these specifications, and the verifier can check the consistency between a program and its specifications.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution
Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 39.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. Abrial, J.-R.: The B-Book: Assigning Programs to Meanings. Cambridge University Press, Cambridge (1996)

    Book  MATH  Google Scholar 

  2. Ambler, A.L., Good, D.I., Browne, J.C., Burger, W.F., Cohen, R.M., Hoch, C.G., Wells, R.E.: GYPSY: A language for specification and implementation of verifiable programs. SIGPLAN Notices 12(3), 1–10 (1977)

    Article  Google Scholar 

  3. Barnes, J.: High Integrity Software: The SPARK Approach to Safety and Security. Addison-Wesley, With Praxis Critical Systems Limited (2003)

    Google Scholar 

  4. Barnett, M., DeLine, R., Fähndrich, M., Leino, K.R.M., Schulte, W.: Verification of object-oriented programs with invariants. Journal of Object Technology 3(6), 27–56 (2004)

    Article  Google Scholar 

  5. Barnett, M., Grieskamp, W., Kerer, C., Schulte, W., Szyperski, C., Tillmann, N., Watson, A.: Serious specification for composing components. In: Crnkovic, I., Schmidt, H., Stafford, J., Wallnau, K. (eds.) Proceedings of the 6th ICSE Workshop on Component-Based Software Engineering: Automated Reasoning and Prediction (May 2003)

    Google Scholar 

  6. Barnett, M., Grieskamp, W., Nachmanson, L., Schulte, W., Tillmann, N., Veanes, M.: Towards a tool environment for model-based testing with AsmL. In: 3rd International Workshop on Formal Approaches to Testing of Software, FATES 2003 (October 2003)

    Google Scholar 

  7. Barnett, M., Naumann, D.A.: Friends need a bit more: Maintaining invariants over shared state. In: Kozen, D. (ed.) Mathematics of Program Construction. LNCS, pp. 54–84. Springer, Heidelberg (2004)

    Chapter  Google Scholar 

  8. Barnett, M., Naumann, D.A., Schulte, W., Sun, Q.: 99.44% pure: Useful abstractions in specifications. In: Poll, E. (ed.) Proceedings of the ECOOP Workshop FTfJP 2004, Formal Techniques for Java-like Programs, pp. 11–19. University of Nijmegen (June 2004), NIII report NIII-R0426

    Google Scholar 

  9. Barnett, M., Schulte, W.: The ABCs of specification: AsmL, behavior, and components. Informatica 25(4), 517–526 (2001)

    MATH  Google Scholar 

  10. Barnett, M., Schulte, W.: Runtime verification of .NET contracts. The Journal of Systems and Software 65(3), 199–208 (2003)

    Google Scholar 

  11. Box, D.: Essential .NET, Volume I: The Common Language Runtime. Addison-Wesley, Reading (2002)

    Google Scholar 

  12. Boyapati, C., Lee, R., Rinard, M.: Ownership types for safe programming: Preventing data races and deadlocks. In: Proceedings of the 2002 ACM SIGPLAN Conference on Object-Oriented Programming Systems, Languages and Applications, OOPSLA 2002. SIGPLAN Notices, vol. 37(11), pp. 211–230. ACM, New York (2002)

    Chapter  Google Scholar 

  13. Burdy, L., Cheon, Y., Cok, D.R., Ernst, M.D., Kiniry, J.R., Leavens, G.T., Leino, K.R.M., Poll, E.: An overview of JML tools and applications. International Journal on Software Tools for Technology Transfer, STTT (2004) (to appear)

    Google Scholar 

  14. Chapman, R.: Industrial experience with SPARK. Presented at SIGAda 2000 (November 2000), Available from, http://www.praxis-cs.co.uk

  15. Cheon, Y.: A Runtime Assertion Checker for the Java Modeling Language. PhD thesis, Iowa State University, Iowa State University, Department of Computer Science. Technical Report TR #03-09 (April 2003)

    Google Scholar 

  16. Cousot, P., Cousot, R.: Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints. In: Conference Record of the Fourth Annual ACM Symposium on Principles of Programming Languages, pp. 238–252. ACM, New York (1977)

    Google Scholar 

  17. DeLine, R., Fähndrich, M.: Enforcing high-level protocols in low-level software. In: Proceedings of the 2001 ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI). SIGPLAN Notices, vol. 36(5), pp. 59–69. ACM, New York (2001)

    Chapter  Google Scholar 

  18. DeLine, R., Fähndrich, M.: Typestates for objects. In: Odersky, M. (ed.) ECOOP 2004. LNCS, vol. 3086, pp. 465–490. Springer, Heidelberg (2004)

    Chapter  Google Scholar 

  19. Detlefs, D., Nelson, G., Saxe, J.B.: Simplify: A theorem prover for program checking. Technical Report HPL-2003-148, HP Labs (July 2003)

    Google Scholar 

  20. Detlefs, D.L., Leino, K.R.M., Nelson, G., Saxe, J.B.: Extended static checking. Research Report 159, Compaq Systems Research Center (December 1998)

    Google Scholar 

  21. Deutsch, L.P.: An Interactive Program Verifier. PhD thesis, University of California, Berkeley (1973)

    Google Scholar 

  22. Dhara, K.K., Leavens, G.T.: Forcing behavioral subtyping through specification inheritance. In: Proceedings 18th International Conference on Software Engineering, pp. 258–267. IEEE, Los Alamitos (1996)

    Chapter  Google Scholar 

  23. Fähndrich, M., Leino, K.R.M.: Declaring and checking non-null types in an object-oriented language. In: Proceedings of the 2003 ACM Conference on Object-Oriented Programming, Systems, Languages, and Applications, OOPSLA 2003. SIGPLAN Notices, vol. 38(11), pp. 302–312. ACM, New York (2003)

    Chapter  Google Scholar 

  24. Findler, R.B., Felleisen, M.: Contract soundness for object-oriented languages. In: Proceedings of the 2001 ACM SIGPLAN Conference on Object-Oriented Programming Systems, Languages and Applications, OOPSLA 2001. SIGPLAN Notices, vol. 36(11), pp. 1–15. ACM, New York (2001)

    Chapter  Google Scholar 

  25. Flanagan, C., Leino, K.R.M., Lillibridge, M., Nelson, G., Saxe, J.B., Stata, R.: Extended static checking for Java. In: Proceedings of the 2002 ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI). SIGPLAN Notices, vol. 37(5), pp. 234–245. ACM, New York (2002)

    Chapter  Google Scholar 

  26. Floyd, R.W.: Assigning meanings to programs. In: Mathematical Aspects of Computer Science, Proceedings of Symposium in Applied Mathematics, vol. 19, pp. 19–32. American Mathematical Society (1967)

    Google Scholar 

  27. German, S.M.: Automating proofs of the absence of common runtime errors. In: Conference Record of the Fifth Annual ACMSymposium on Principles of Programming Languages, pp. 105–118 (1978)

    Google Scholar 

  28. Good, D.I., London, R.L., Bledsoe, W.W.: An interactive program verification system. In: Proceedings of the international conference on Reliable software, pp. 482–492. ACM, New York (1975)

    Chapter  Google Scholar 

  29. Goodenough, J.B.: Structured exception handling. In: Conference Record of the Second ACM Symposium on Principles of Programming Languages, pp. 204–224. ACM, New York (1975)

    Google Scholar 

  30. Gosling, J., Joy, B., Steele, G.: The JavaTM Language Specification. Addison- Wesley, Reading (1996)

    MATH  Google Scholar 

  31. Grieskamp, W., Tillmann, N., Veanes, M.: Instrumenting scenarios in a model-driven development environment. Submitted manuscript (2004)

    Google Scholar 

  32. Guaspari, D., Marceau, C., Polak, W.: Formal verification of Ada programs. IEEE Transactions on Software Engineering 16(9), 1058–1075 (1990)

    Article  Google Scholar 

  33. Gurevich, Y., Rossman, B., Schulte, W.: Semantic essence of AsmL. Theoretical Computer Science (2005) (to appear)

    Google Scholar 

  34. Hoare, C.A.R.: An axiomatic approach to computer programming. Communications of the ACM 12, 576–580, 583 (1969)

    Article  MATH  Google Scholar 

  35. Hoare, C.A.R.: Monitors: an operating system structuring concept. Communications of the ACM 17(10), 549–557 (1974)

    Article  MATH  Google Scholar 

  36. Jacobs, B., Rustan, K., Leino, M., Schulte, W.: Verification of multithreaded objectoriented programs with invariants. In: Proceedings of the workshop on Specification and Verification of Component-Based Systems (2004) (to appear)

    Google Scholar 

  37. King, J.C.: Symbolic execution and program testing. Communications of the ACM 19(7), 385–394 (1976)

    Article  MATH  Google Scholar 

  38. King, J.C.: A Program Verifier. PhD thesis, Carnegie-Mellon University (September 1969)

    Google Scholar 

  39. Lampson, B.W., Horning, J.J., London, R.L., Mitchell, J.G., Popek, G.J.: Report on the programming language Euclid. Technical Report CSL-81-12, Xerox PARC (October 1981); An earlier version of this report appeared. In: SIGPLAN Notices, vol. 12(2). ACM, New York (February 1977)

    Google Scholar 

  40. Leavens, G.T., Baker, A.L., Ruby, C.: JML: A notation for detailed design. In: Kilov, H., Rumpe, B., Simmonds, I. (eds.) Behavioral Specifications of Businesses and Systems, pp. 175–188. Kluwer Academic Publishers, Dordrecht (1999)

    Google Scholar 

  41. Leavens, G.T., Baker, A.L., Ruby, C.: Preliminary design of JML: A behavioral interface specification language for Java. Technical Report 98-06u, Iowa State University, Department of Computer Science (April 2003)

    Google Scholar 

  42. Rustan, K., Leino, M.: Data groups: Specifying the modification of extended state. In: Proceedings of the 1998 ACM SIGPLAN Conference on Object-Oriented Programming Systems, Languages and Applications (OOPSLA 1998). SIGPLAN Notices, vol. 33(10), pp. 144–153. ACM, New York (1998)

    Google Scholar 

  43. Rustan, K., Leino, M.: Extended static checking: A ten-year perspective. In: Wilhelm, R. (ed.) Informatics: 10 Years Back, 10 Years Ahead. LNCS, vol. 2000, pp. 157–175. Springer, Heidelberg (2001)

    Chapter  Google Scholar 

  44. Rustan, K., Leino, M., Millstein, T., Saxe, J.B.: Generating error traces from verification-condition counterexamples. Science of Computer Programming (2004) (to appear)

    Google Scholar 

  45. Rustan, K., Leino, M., Müller, P.: Modular verification of global module invariants in object-oriented programs. Technical Report 459, ETH Zürich (September 2004)

    Google Scholar 

  46. Rustan, K., Leino, M., Müller, P.: Object invariants in dynamic contexts. In: Odersky, M. (ed.) ECOOP 2004. LNCS, vol. 3086, pp. 491–516. Springer, Heidelberg (2004)

    Chapter  Google Scholar 

  47. Rustan, K., Leino, M., Nelson, G.: Data abstraction and information hiding. ACM Transactions on Programming Languages and Systems 24(5), 491–553 (2002)

    Article  Google Scholar 

  48. Rustan, K., Leino, M., Saxe, J.B., Stata, R.: Checking Java programs via guarded commands. In: Jacobs, B., Leavens, G.T., Müller, P., Poetzsch-Heffter, A. (eds.) Formal Techniques for Java Programs. Technical Report 251. Fernuniversität Hagen (May 1999)

    Google Scholar 

  49. Rustan, K., Leino, M., Schulte, W.: Exception safety for C#. In: SEFM 2004—Second International Conference on Software Engineering and Formal Methods, pp. 218–227. IEEE, Los Alamitos (2004)

    Chapter  Google Scholar 

  50. Liskov, B., Guttag, J.: Abstraction and Specification in Program Development. In: MIT Electrical Engineering and Computer Science Series. MIT Press, Cambridge (1986)

    Google Scholar 

  51. Luckham, D.C.: Programming with Specifications: An Introduction to Anna, a Language for Specifying Ada Programs. In: Texts and Monographs in Computer Science. Springer, Heidelberg (1990)

    Google Scholar 

  52. Luckham, D.C., German, S.M., von Henke, F.W., Karp, R.A., Milne, P.W., Oppen, D.C., Polak, W., Scherlis, W.L.: Stanford Pascal Verifier user manual. Technical Report STANCS-79-731, Stanford University (1979)

    Google Scholar 

  53. Mann, C.C.: Why software is so bad. MIT Technology Review (July/August 2002)

    Google Scholar 

  54. McConnell, S.: Code complete: A practical handbook of software construction. Microsoft Press (1993)

    Google Scholar 

  55. Meyer, B.: Object-oriented software construction. Series in Computer Science. Prentice-Hall International, Englewood Cliffs (1988)

    Google Scholar 

  56. Müller, P.: Modular Specification and Verification of Object-Oriented Programs. In: Müller, P. (ed.) Modular Specification and Verification of Object-Oriented Programs. LNCS, vol. 2262, p. 123. Springer, Heidelberg (2002); PhD thesis, FernUniversität Hagen

    Google Scholar 

  57. RTI Health, Social, and Economic Research. The economic impact of inadequate infrastructure for software testing. RTI Project 7007.011, National Institute for Standards and Technology (May 2002)

    Google Scholar 

  58. Sagiv, M., Reps, T., Horwitz, S.: Precise interprocedural dataflow analysis with applications to constant propagation. Theoretical Computer Science 167(1-2), 131–170 (1996)

    Article  MATH  MathSciNet  Google Scholar 

  59. Sălcianu, A., Rinard, M.: A combined pointer and purity analysis for Java programs. Technical Report MIT-CSAIL-TR-949, MIT (May 2004)

    Google Scholar 

  60. Sites, R.L.: Proving that Computer Programs Terminate Cleanly. PhD thesis, Stanford University, Technical Report STAN-CS-74-418 (May 1974)

    Google Scholar 

  61. van den Berg, J., Jacobs, B.: The LOOP compiler for java and JML. In: Margaria, T., Yi, W. (eds.) TACAS 2001. LNCS, vol. 2031, pp. 299–312. Springer, Heidelberg (2001)

    Chapter  Google Scholar 

  62. Williams, M.: Microsoft Visual C# .NET. Microsoft Press (2002)

    Google Scholar 

  63. Wing, J.M.: A two-tiered approach to specifying programs. PhD thesis, MIT Department of Electrical Engineering and Computer Science, MIT Laboratory for Computer Science TR-299 (May 1983)

    Google Scholar 

  64. Wulf, W.A., London, R.L., Shaw, M.: An introduction to the construction and verification of Alphard programs. IEEE Transactions on Software Engineering SE- 2(4), 253–265 (1976)

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Microsoft Research, Redmond, WA, USA

    Mike Barnett, K. Rustan M. Leino & Wolfram Schulte

Authors
  1. Mike Barnett
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. K. Rustan M. Leino
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Wolfram Schulte
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. IMDEA Software, Madrid, Spain

    Gilles Barthe

  2. INRIA Sophia Antipolis, France

    Lilian Burdy  & Marieke Huisman  & 

  3. Gemalto, France

    Jean-Louis Lanet

  4. Ecole Supérieure D’Ingénieurs de Luminy - Case 925 - ESIL Parc Scientifique, Université de la Méditerranée, 13288, Marseille, France

    Traian Muntean

Rights and permissions

Reprints and permissions

Copyright information

© 2005 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Barnett, M., Leino, K.R.M., Schulte, W. (2005). The Spec# Programming System: An Overview. In: Barthe, G., Burdy, L., Huisman, M., Lanet, JL., Muntean, T. (eds) Construction and Analysis of Safe, Secure, and Interoperable Smart Devices. CASSIS 2004. Lecture Notes in Computer Science, vol 3362. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-30569-9_3

Download citation

  • DOI: https://doi.org/10.1007/978-3-540-30569-9_3

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-24287-1

  • Online ISBN: 978-3-540-30569-9

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation