Inculcating invariants in introductory courses

ABSTRACT

One goal of introductory software engineering courses is to motivate and instill good software engineering habits. Unfortunately, practical constraints on typical courses often lead to student experiences that are antithetical to that goal: instead of working in large teams and dealing with changing requirements and maintaining programs over many years, courses generally involve students working alone or in small teams with short projects that end the first time the program works correctly on some selected input. Small projects tend to reinforce poor software engineering practices. Since the programs are small enough to manage cognitively in ad hoc ways, effort spent more precisely documenting assumptions seems wasteful. It is infeasible to carry out full industrial software development within the context of a typical university course. However, it is possible to simulate some aspects of safety critical software engineering in an introductory software engineering course. This paper describes an approach that focuses on thinking about and precisely documenting invariants, and checking invariants using lightweight analysis tools. We describe how assignments were designed to emphasize the importance of invariants and to incorporate program analysis tools with typical software engineering material and report on results from an experiment measuring students understanding of program invariants.

REFERENCES

• 1: Mike Barnett, K. Rustan M. Leino, and Wolfram Schulte. The Spec# Programming System: An Overview. Construction and Analysis of Safe, Secure, and Interoperable Smart Devices, LNCS Volume 3362, Spring 2004.
• 2: Edsger Wybe Dijkstra, A Discipline of Programming, Prentice Hall PTR, Upper Saddle River, NJ, 1997
• 3: Object Technology International. Eclipse Platform Technical Overview. Feb 2003. http://www.eclipse.org/whitepapers/eclipse-overview.pdf
• 4: Michael Dean Ernst , David Notkin, Dynamically discovering likely program invariants, 2000
• 5: Michael D. Ernst , Jake Cockrell , William G. Griswold , David Notkin, Dynamically Discovering Likely Program Invariants to Support Program Evolution, IEEE Transactions on Software Engineering, v.27 n.2, p.99-123, February 2001 [doi>10.1109/32.908957]
• 6: David Evans , John Guttag , James Horning , Yang Meng Tan, LCLint: a tool for using specifications to check code, Proceedings of the 2nd ACM SIGSOFT symposium on Foundations of software engineering, p.87-96, December 06-09, 1994, New Orleans, Louisiana, United States
• 7: David Evans, Static detection of dynamic memory errors, Proceedings of the ACM SIGPLAN 1996 conference on Programming language design and implementation, p.44-53, May 21-24, 1996, Philadelphia, Pennsylvania, United States
• 8: David Evans , David Larochelle, Improving Security Using Extensible Lightweight Static Analysis, IEEE Software, v.19 n.1, p.42-51, January 2002 [doi>10.1109/52.976940]
• 9: Google Web APIs. http://www.google.com/apis/
• 10: David Gries, The Science of Programming, Springer-Verlag New York, Inc., Secaucus, NJ, 1987
• 11: K. Rustan M. Leino, Extended Static Checking: A Ten-Year Perspective, Informatics - 10 Years Back. 10 Years Ahead., p.157-175, January 2001
• 12: Barbara Liskov , John Guttag, Program Development in Java: Abstraction, Specification, and Object-Oriented Design, Addison-Wesley Longman Publishing Co., Inc., Boston, MA, 2000
• 13: Jeremy W. Nimmer and Michael D. Ernst. Static verification of dynamically detected program invariants: Integrating Daikon and ESC/Java. First Workshop on Runtime Verification, July, 2001.
• 14: Jeremy W. Nimmer , Michael D. Ernst, Invariant inference for static checking:, Proceedings of the 10th ACM SIGSOFT symposium on Foundations of software engineering, November 18-22, 2002, Charleston, South Carolina, USA [doi>10.1145/587051.587054]
• 15: Mark Allen Weiss. Data Structures and Algorithm Analysis in Java. Addison Wesley Longman, 1999.
• 16: Jeannette M. Wing, Invited Talk: Weaving Formal Methods into the Undergraduate Computer Science Curriculum, Proceedings of the 8th International Conference on Algebraic Methodology and Software Technology, p.2-9, May 20-27, 2000
• 17: Jinlin Yang , David Evans, Dynamically inferring temporal properties, Proceedings of the ACM-SIGPLAN-SIGSOFT workshop on Program analysis for software tools and engineering, June 07-08, 2004, Washington DC, USA [doi>10.1145/996821.996832]
• 18: Jinlin Yang , David Evans, Automatically Inferring Temporal Properties for Program Evolution, Proceedings of the 15th International Symposium on Software Reliability Engineering (ISSRE'04), p.340-351, November 02-05, 2004 [doi>10.1109/ISSRE.2004.11]
• 19: Jinlin Yang , David Evans , Deepali Bhardwaj , Thirumalesh Bhat , Manuvir Das, Perracotta: mining temporal API rules from imperfect traces, Proceeding of the 28th international conference on Software engineering, May 20-28, 2006, Shanghai, China [doi>10.1145/1134285.1134325]

INDEX TERMS

Primary Classification:
  D. Software
  D.2 SOFTWARE ENGINEERING
      D.2.4 Software/Program Verification
          Subjects: Assertion checkers

Additional Classification:
  D. Software
  D.2 SOFTWARE ENGINEERING
      D.2.4 Software/Program Verification
          Subjects: Class invariants; Programming by contract; Formal methods; Reliability

  F. Theory of Computation
  F.3 LOGICS AND MEANINGS OF PROGRAMS
      F.3.1 Specifying and Verifying and Reasoning about Programs
          Subjects: Invariants; Pre- and post-conditions; Assertions; Specification techniques; Mechanical verification; Logics of programs

  K. Computing Milieux
  K.3 COMPUTERS AND EDUCATION
      K.3.2 Computer and Information Science Education

General Terms:
Reliability, Security, Verification

Keywords:
dependability, dynamic inference, introductory software engineering, invariants, security, software engineering, static analysis