Formal Reasoning Using an Iterative Approach with an Integrated Web IDE

Nabil M. Kabbani
(Clemson University)
Daniel Welch
(Clemson University)
Caleb Priester
(Clemson University)
Stephen Schaub
(Clemson University)
Blair Durkee
(Clemson University)
Yu-Shan Sun
(Clemson University)
Murali Sitaraman
(Clemson University)

This paper summarizes our experience in communicating the elements of reasoning about correctness, and the central role of formal specifications in reasoning about modular, component-based software using a language and an integrated Web IDE designed for the purpose. Our experience in using such an IDE, supported by a 'push-button' verifying compiler in a classroom setting, reveals the highly iterative process learners use to arrive at suitably specified, automatically provable code. We explain how the IDE facilitates reasoning at each step of this process by providing human readable verification conditions (VCs) and feedback from an integrated prover that clearly indicates unprovable VCs to help identify obstacles to completing proofs. The paper discusses the IDE's usage in verified software development using several examples drawn from actual classroom lectures and student assignments to illustrate principles of design-by-contract and the iterative process of creating and subsequently refining assertions, such as loop invariants in object-based code.

In Catherine Dubois, Paolo Masci and Dominique Méry: Proceedings Second International Workshop on Formal Integrated Development Environment (F-IDE 2015), Oslo, Norway, June 22, 2015, Electronic Proceedings in Theoretical Computer Science 187, pp. 56–71.
Published: 14th August 2015.

ArXived at: http://dx.doi.org/10.4204/EPTCS.187.5 bibtex PDF
References in reconstructed bibtex, XML and HTML format (approximated).
Comments and questions to: eptcs@eptcs.org
For website issues: webmaster@eptcs.org