NameDateSize

..14-Nov-201914

HolmakefileH A D25-Jul-2019420

m1_factorial_proofScript.smlH A D25-Jul-20192 KiB

m1_factorialScript.smlH A D25-Jul-20192 KiB

m1_progLib.sigH A D25-Jul-2019114

m1_progLib.smlH A D25-Jul-20195.3 KiB

m1_progScript.smlH A D25-Jul-201929.4 KiB

MakefileH A D25-Jul-2019267

READMEH A D25-Jul-2019977

session1.lispH A D25-Jul-2019139

session2.lispH A D25-Jul-201981

README

1
2Overview
3--------
4
5This directory shows how the decompiler from
6
7  HOL/examples/machine-code/decompiler
8
9can be used for the HOL4 version of J's M1 model, which is located at
10
11  HOL/examples/acl2/examples/M1
12
13Typing 'make' should perform the complete proof.
14
15
16Files in this directory
17-----------------------
18
19   README ............................ this file
20
21   Makefile .......................... builds everything in this directory
22   Holmakefile ....................... imports the decompiler and the M1 model
23
24   m1_progScript.sml ................. defines Hoare triples for the M1 model
25   m1_progLib.sml .................... specialises the decompiler to the M1 model
26   m1_factorialScript.sml ............ decompiles the factorial program
27   m1_factorial_proofScript.sml ...... proves that the function produced by 
28                                       decompilation above calculates factorial
29
30   session1.lisp, session2.lisp ...... are files used by the Makefile
31
32
33