README
1Interactive Proofs of Programs
2------------------------------
3
4Author: Stephen Motty
5Supervisor: Theodore Norvell
6Publisher: Memorial University Of Newfoundland
7
8Original Publication Date: October 19, 2010
9
10In his work "A Practical Theory of Programming", Dr. Eric Hehner proposed that
11programs can be treated as mathematical objects. Thus proofs of programs are
12simply mathematical proofs and software that handles proofs in various areas
13of mathematics such as HOL4/Kananaskis can be used for verification that
14programs meet their specifications.
15
16In this directory:
17- ptopScript.sml presents logical definitions for commands such as assignment,
18 and sequential composition. It also provides a definition of software
19 refinement.
20- imperativeLib.sml provides some proof tactics that are useful proving
21 refinement of a logical specification by a program. Programs can be written
22 using any of imperative commands defined in ptopTheory
23- imperativeScript.sml uses tactics to prove laws such as the forwardSubstition
24 law
25- selftest.sml demonstrates the theory as it applies to verifying the
26 correctness of two programs that swap x for y
27- reflectOnFailure.sml demonstrates how the theory detects potential bugs
28 and the process involved in disproving refinement
29
30This example provides updated software originally discused at 2010 NECEC
31conference. NECEC 2010 is a forum where professionals in electrical,
32electronic and computer engineering as well as information technologies can
33present their work to the growing technical community within the province.
34The conference focuses on technical concepts, innovations and implementations.
35The original paper can be obtained from the online archive:
36
37http://necec.engr.mun.ca/ocs2010/viewabstract.php?id=32
38