Toggle Main Menu Toggle Search

Open Access padlockePrints

The Newcastle University research output collection, currently available on ePrints, will shortly be moving to a new open repository platform, Figshare. To prepare for the data migration we have paused adding new content to ePrints, and will resume once the new repository is launched. During this time you will continue to have access to ePrints (but no new content will appear). We will share updates here when available.

Reasoning about programs via operational semantics: requirements for a support system

Lookup NU author(s): John Hughes, Emeritus Professor Cliff JonesORCiD

Downloads

Full text for this publication is not currently held within this repository. Alternative links are provided below where available.

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.

Publication metadata

Author(s): Hughes JRD, Jones CB

Publication type: Article

Publication status: Published

Journal: Automated Software Engineering

Year: 2008

Volume: 15

Issue: 3-4

Pages: 299-312

ISSN (print): 0928-8910

ISSN (electronic): 1573-7535

Publisher: Springer

URL: http://dx.doi.org/10.1007/s10515-008-0036-6

DOI: 10.1007/s10515-008-0036-6

Altmetrics

Altmetrics provided by Altmetric

Share