Computing Preconditions and Postconditions of While Loops

详细信息    查看全文

• 作者：Olfa Mraihi (1) olfa.mraihi@yahoo.fr
  Wided Ghardallou (2) wided.ghardallou@gmail.com
  Asma Louhichi (2) louhichiasma@yahoo.fr
  Lamia Labed Jilani (1) lamia.labed@isg.rnu.tn
  Khaled Bsaies (2) khaled.bsaies@fst.rnu.tn
  Ali Mili (3) mili@cis.njit.edu
• 关键词：weakest precondition – ; strongest postcondition – ; while loop – ; invariant relation – ; programming language semantics – ; program correctness – ; relational calculus
• 刊名：Lecture Notes in Computer Science
• 出版年：2011
• 出版时间：2011
• 年：2011
• 卷：6916
• 期：1
• 页码：173-193
• 全文大小：278.0 KB
• 参考文献：1. Barnett, M., Rustan Leino, K.: Weakest precondition of unstructured programs. In: Proceedings, Sixth ACM SIGPLAN-SIGSOFT Workshop on Program Analysis for Software Tools and Engineering, Lisbon, Portugal (2005)
  2. Berghammer, R.: Soundness of a purely syntactical formalization of weakest preconditions. Electronic Notes in Theoretical Computer Science. Elsevier Science Publisher, Amsterdam (2000)
  3. Boudriga, N., Elloumi, F., Mili, A.: The lattice of specifications: Applications to a specification methodology. Formal Aspects of Computing 4, 544–571 (1992)
  4. Brumley, D., Wang, H., Jha, S., Song, D.: Creating vulnerability signatures using weakest preconditions. In: Proceedings, 20th Computer Security Foundations Symposium, Venice, Italy, pp. 311–325 (2007)
  5. Cavalcanti, A., Naumann, D.: A weakest precondition semantics for refinement of object oriented programs. IEEE Transactions on Software Engineering 26(8), 713–728 (2000)
  6. Costa, M., Castro, M., Zhou, L., Zhang, L., Peinado, M.: Bouncer: Securing software by blocking bad input. In: Proceedings, ACM Symposium on Operating Systems Principles (October 2007)
  7. Dijkstra, E.W.: Guarded commands, non dterminacy, and formal derivation of programs. Communications of the ACM 18(8), 453–457 (1975)
  8. Dijkstra, E.W.: A Discipline of Programming. Prentice-Hall, Englewood Cliffs (1976)
  9. Flanagan, C., Qadeer, S.: Predicate abstraction for software verification. In: Proceedings, POPL 2002: The 29th SIGPLAN-SIGACT Symposium on Principles of Programming Languages (2002)
  10. Flanagan, C., Saxe, J.B.: Avoiding exponential explosion: Generating compact verification conditions. In: Proceedings, Symposium on Principles of Programming Languages (2001)
  11. Gannod, G.C., Cheng, B.H.C.: Strongest postcondition semantics as the formal basis for reverse engineering. In: Proceedings, Second Working Conference on Reverse Engineering, Toronto, Ontario, Canada, pp. 188–197 (1995)
  12. Gries, D.: The Science of programming. Springer, Heidelberg (1981)
  13. Grigore, R., Charles, J., Fairmichael, F., Kiniry, J.: Strongest postcondition of unstructured programs. In: Proceedings of the 11th International Workshop on Formal Techniques for Java-like Programs (2009)
  14. Gulwani, S., Srivastava, S., Venkatesan, R.: Program analysis as constraint solving. In: Proceedings, PLDI 2008: ACM SIGPLAN 2008 Conference on Programming Languages and their Implementation, Tuscon, AZ (2008)
  15. Hoare, C.A.R.: An axiomatic basis for computer programming. Communications of the ACM 12(10), 576–583 (1969)
  16. Jager, I., Brumley, D.: Efficient directionless weakest preconditions. Technical Report CMU-CyLab-10-002, Carnegie Mellon University (February 2010)
  17. Leino, K.R.M.: Efficient weakest preconditions. Information Processing Letters 93(6), 281–288 (2005)
  18. Leino, K.R.: Towards reliable modular programs. Technical report, California Institute of Technology, Pasadena, CA (1995)
  19. Louhichi, A., Mraihi, O., Jilani, L.L., Mili, A.: Invariant assertions, invariant relations and invariant functions. In: Proceedings, 2nd International Workshop on Invariant Generation, York, UK (2009)
  20. Manna, Z.: A Mathematical Theory of Computation. McGraw-Hill, New York (1974)
  21. Mili, A., Aharon, S., Nadkarni, C.: Mathematics for reasoning about loop. Science of Computer Programming, 989–1020 (2009)
  22. Morgan, C.C.: Programming from Specifications. International Series in Computer Sciences. Prentice Hall, London (1998)
  23. Necula, G.C.: Proof carrying code. In: Proceedings, Symposium on Principles of Programming Languages (1997)
  24. Rauch, N.: Precondition generation for a Java subset. In: Proceedings, FM-TOOLS 2002: The Fifth Workshop on Tools for System Design and Verification, Reisensberg, Germany (2002)
  25. von Oheimb, D.: Analyzing java in isabelle/hol: Formalization, type safety, and hoare logic. Technical report, Technische Universitaet Muenchen (2001)
• 作者单位：1. Institut Superieur de Gestion, Tunis, Tunisia2. Faculte des Sciences de Tunis, El Manar, Tunisia3. NJIT, Newark, NJ, USA
• 刊物类别：Computer Science
• 刊物主题：Artificial Intelligence and Robotics
  Computer Communication Networks
  Software Engineering
  Data Encryption
  Database Management
  Computation by Abstract Devices
  Algorithm Analysis and Problem Complexity
  
• 出版者：Springer Berlin / Heidelberg
• ISSN：1611-3349

文摘

Weakest preconditions were introduced by Dijkstra as a tool to define the semantics of programming constructs, and thereby as a means to prove the correctness of programs; the dual concept of strongest postcondition was introduced subsequently as an alternative means for the same ends. In this paper, we present and discuss a method to compute weakest preconditions and strongest postconditions of while loops in a C-like programming language; to this effect, we use the concept of invariant relation. Whereas the task of computing weakest preconditions and strongest postconditions of while loops is usually approached by limiting the number of iterations and applying successive sequential compositions, invariant relations afford us a crisper, closed form solution.