%0 Journal Article %1 hughes_08_reasoning %A Hughes, John %A Jones, Cliff %D 2008 %J Automated Software Engineering %K 2008 _hardcopy reasoning semantics operational %N 3-4 %P 299--312 %R http://dx.doi.org/10.1007/s10515-008-0036-6 %T Reasoning about programs via operational semantics: requirements for a support system %U http://dx.doi.org/10.1007/s10515-008-0036-6 %V 15 %X Abstract  Reasoning about programs using ^a€oeaxioms^a€� 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.

@article{hughes_08_reasoning, abstract = {Abstract  Reasoning about programs using ^{a}€{oe}axioms^{a}€� 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.}, added-at = {2009-02-11T20:14:36.000+0100}, author = {Hughes, John and Jones, Cliff}, biburl = {https://www.bibsonomy.org/bibtex/2eb374458530c79730836ca57934a7875/leonardo}, citeulike-article-id = {3384492}, doi = {http://dx.doi.org/10.1007/s10515-008-0036-6}, interhash = {277afe273ed1302176f58bae0f07459e}, intrahash = {eb374458530c79730836ca57934a7875}, journal = {Automated Software Engineering}, keywords = {2008 _hardcopy reasoning semantics operational}, month = {December}, number = {3-4}, pages = {299--312}, posted-at = {2008-10-07 21:42:04}, priority = {4}, timestamp = {2009-02-11T20:14:36.000+0100}, title = {Reasoning about programs via operational semantics: requirements for a support system}, url = {http://dx.doi.org/10.1007/s10515-008-0036-6}, volume = 15, year = 2008 }