NameDateSize

..25-Jul-201958

HolmakefileH A D25-Jul-2019307

imperativeLib.sigH A D25-Jul-20191.1 KiB

imperativeLib.smlH A D25-Jul-20194.5 KiB

imperativeScript.smlH A D25-Jul-201930.2 KiB

necec2010.smlH A D25-Jul-201925.6 KiB

ptopScript.smlH A D25-Jul-20191.5 KiB

READMEH A D25-Jul-20191.7 KiB

reflectOnFailure.smlH A D25-Jul-201910.9 KiB

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