Theory of Designs in Isabelle/UTP

Simon David Foster; Yakoub Nemouchi; Frank Zeyda

Theory of Designs in Isabelle/UTP

Simon David Foster, Yakoub Nemouchi, Frank Zeyda

Computer Science

Research output: Working paper

Abstract

This document describes a mechanisation of the UTP theory of designs in Isabelle/UTP. Designs enrich UTP relations with explicit precondition/postcondition pairs, as present in formal notations like VDM, B, and the refinement calculus. If a program’s precondition holds, then it is guaranteed to terminate and establish its postcondition, which is an approach known as total correctness. If the precondition does not hold, the behaviour is maximally nondeterministic, which represents unspecified behaviour. In this mechanisation, we create the theory of designs, including its alphabet, signature, and healthiness conditions. We then use these to prove the key algebraic laws of programming. This development can be used to support program verification based on total correctness.

Original language	English
Number of pages	47
Publication status	Unpublished - 6 Apr 2018

Access to Document

UTP-Designs

Cite this

@techreport{cb2d178f9b174b2dbcd993a5141a3db7,

title = "Theory of Designs in Isabelle/UTP",

abstract = "This document describes a mechanisation of the UTP theory of designs in Isabelle/UTP. Designs enrich UTP relations with explicit precondition/postcondition pairs, as present in formal notations like VDM, B, and the refinement calculus. If a program{\textquoteright}s precondition holds, then it is guaranteed to terminate and establish its postcondition, which is an approach known as total correctness. If the precondition does not hold, the behaviour is maximally nondeterministic, which represents unspecified behaviour. In this mechanisation, we create the theory of designs, including its alphabet, signature, and healthiness conditions. We then use these to prove the key algebraic laws of programming. This development can be used to support program verification based on total correctness.",

author = "Foster, {Simon David} and Yakoub Nemouchi and Frank Zeyda",

year = "2018",

month = apr,

day = "6",

language = "English",

type = "WorkingPaper",

}

TY - UNPB

T1 - Theory of Designs in Isabelle/UTP

AU - Foster, Simon David

AU - Nemouchi, Yakoub

AU - Zeyda, Frank

PY - 2018/4/6

Y1 - 2018/4/6

N2 - This document describes a mechanisation of the UTP theory of designs in Isabelle/UTP. Designs enrich UTP relations with explicit precondition/postcondition pairs, as present in formal notations like VDM, B, and the refinement calculus. If a program’s precondition holds, then it is guaranteed to terminate and establish its postcondition, which is an approach known as total correctness. If the precondition does not hold, the behaviour is maximally nondeterministic, which represents unspecified behaviour. In this mechanisation, we create the theory of designs, including its alphabet, signature, and healthiness conditions. We then use these to prove the key algebraic laws of programming. This development can be used to support program verification based on total correctness.

AB - This document describes a mechanisation of the UTP theory of designs in Isabelle/UTP. Designs enrich UTP relations with explicit precondition/postcondition pairs, as present in formal notations like VDM, B, and the refinement calculus. If a program’s precondition holds, then it is guaranteed to terminate and establish its postcondition, which is an approach known as total correctness. If the precondition does not hold, the behaviour is maximally nondeterministic, which represents unspecified behaviour. In this mechanisation, we create the theory of designs, including its alphabet, signature, and healthiness conditions. We then use these to prove the key algebraic laws of programming. This development can be used to support program verification based on total correctness.

M3 - Working paper

BT - Theory of Designs in Isabelle/UTP

ER -