Back to Search
Start Over
Reasoning about programs via operational semantics: requirements for a support system.
- Source :
- Automated Software Engineering; Dec2008, Vol. 15 Issue 3/4, p299-312, 14p
- Publication Year :
- 2008
-
Abstract
- Reasoning about programs using "axioms" is well established; in this paper we argue that reasoning about a program directly in terms of Structural Operational Semantic (SOS) language descriptions is a viable addition and that this is anyway necessary for the vast majority of languages where there is nothing like a full axiomatic description. Using an SOS description is likely to require detailed proofs whose acceptability to users will depend on suitable support systems. The paper presents a very simple example to illustrate how we can reason about (in fact, develop) a program to prove that it satisfies a specification. The main contribution is to use this trivial example to point out issues in designing an interactive proof system for constructing such proofs. [ABSTRACT FROM AUTHOR]
Details
- Language :
- English
- ISSN :
- 09288910
- Volume :
- 15
- Issue :
- 3/4
- Database :
- Complementary Index
- Journal :
- Automated Software Engineering
- Publication Type :
- Academic Journal
- Accession number :
- 35564889
- Full Text :
- https://doi.org/10.1007/s10515-008-0036-6