Name | Date | Size | ||
---|---|---|---|---|
.. | 14-Nov-2019 | 14 | ||
Holmakefile | H A D | 25-Jul-2019 | 420 | |
m1_factorial_proofScript.sml | H A D | 25-Jul-2019 | 2 KiB | |
m1_factorialScript.sml | H A D | 25-Jul-2019 | 2 KiB | |
m1_progLib.sig | H A D | 25-Jul-2019 | 114 | |
m1_progLib.sml | H A D | 25-Jul-2019 | 5.3 KiB | |
m1_progScript.sml | H A D | 25-Jul-2019 | 29.4 KiB | |
Makefile | H A D | 25-Jul-2019 | 267 | |
README | H A D | 25-Jul-2019 | 977 | |
session1.lisp | H A D | 25-Jul-2019 | 139 | |
session2.lisp | H A D | 25-Jul-2019 | 81 |
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