School of Computing - University of Teesside - Middlesbrough (UK)

Menu of Content

General Correctness

A valuable division of contractual responsibilities between the programmer who implements an operation and the programmer who invokes it is provided by the operation's pre-condition. The implementer is free to write his code under the assumption that the pre-condition will hold, and the user's code must ensure that this is, indeed, the case. The usual approach for logical analysis of pre-conditions is known as total correctness and takes the view that nothing can be proved about an operation invoked outside its pre-condition: it may terminate with any value, may fail to terminate, or may destroy the machine on which it runs. A more general approach is that of General Correctness, which allows us to describe all the operations that total correctness can describe, but also allows us to give guarantees about what the result of executing an operation outside its pre-condition will be should that operation terminate. Amongst the topics we investigate are the specification (whilst preserving monotonicity of refinement) of concurrent operations running under a termination pact and Prescriptions which are the General Correctness formulation of Hoare-He Designs.

  1. S. E. Dunne. Junctive compositions of specifications in total and general correctness. In J. Derrick, E. Boiten, J. C. P. Woodcock, and J. von Wright, editors, Refine 2002: The BCS FACS Refinement Workshop, volume 70 of Electronic Notes in Theoretical Computer Science. Elsevier Science BV, 2002. http://www.elsevier.nl/locate/entcs.
  2. S. E. Dunne. Abstract commands: a uniform notation for specifications and implementations. In C. J. Fidge, editor, Computing: The Australasian Theory Symposium (CATS 2001), volume 42 of Electronic Notes in Theoretical Computer Science. Elsevier Science BV, 2001. http://www.elsevier.nl/locate/entcs.
  3. S. E. Dunne. Recasting Hoare and He's unifying theory of programs in the context of general correctness. In A. Butterfield, G. Strong, and C. Pahl, editors, Proceedings of the 5th Irish Workshop in Formal Methods, IWFM 2001, Workshops in Computing. British Computer Society, 2001. http://ewic.bcs.org/conferences/2001/5thformal/papers.
  4. S. E. Dunne, W. J. Stoddart, and A. J. Galloway. Specification and refinement in general correctness. In A. Evans, D. Duke, and A. Clark, editors, Proceedings of the 3rd Northern Formal Methods Workshop. BCS Electronic Workshops in Computing, 1998. http://www.ewic.org.uk/ewic/workshop/view.cfm/NFM-98.
  5. S. E. Dunne, W. J. Stoddart, and A. J. Galloway. Hypersubstitutions: extending the generalised substitution to model semi-decidable operations. In H. Habrias, editor, The First B Conference. Universite de Nantes, 1996. ISBN 2-906082-25-2.
If you have difficulties accessing this website please email d.cumbor {at} tees.ac.uk.