Formal Reasoning Using an Iterative Approach with an Integrated Web IDE

Autor: Caleb H. Priester, Stephen Schaub, Murali Sitaraman, Danny R. Welch, Yu-Shan Sun, Nabil M. Kabbani, Blair Durkee
Jazyk: angličtina
Rok vydání: 2015
Předmět:
FOS: Computer and information sciences
Loop invariant
Correctness
Computer science
Computer Science - Human-Computer Interaction
02 engineering and technology
computer.software_genre
lcsh:QA75.5-76.95
Human-Computer Interaction (cs.HC)
Computer Science - Software Engineering
Software
Formal specification
Component (UML)
0202 electrical engineering
electronic engineering
information engineering
Iterative and incremental development
Computer Science - Programming Languages
business.industry
Programming language
lcsh:Mathematics
Software development
020207 software engineering
lcsh:QA1-939
Software Engineering (cs.SE)
TheoryofComputation_LOGICSANDMEANINGSOFPROGRAMS
020201 artificial intelligence & image processing
lcsh:Electronic computers. Computer science
Compiler
business
computer
Programming Languages (cs.PL)
Zdroj: F-IDE
Electronic Proceedings in Theoretical Computer Science, Vol 187, Iss Proc. F-IDE 2015, Pp 56-71 (2015)
Popis: 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 Proceedings F-IDE 2015, arXiv:1508.03388
Databáze: OpenAIRE
Externí odkaz: