Lightweight Java (LJ)
=====================
Information about LJ
--------------------
Please see the Isabelle-generated PDF
and/or
http://rok.strnisa.com/lj/
Overview of files
-----------------
├── IsaMakefile (
"Isabelle makefile to verify the theories, and to
create a PDF within the 'document' directory.")
├── Lightweight_Java_Definition.thy (
"The Ott-generated Isabelle2011
definition of LJ.")
├── Lightweight_Java_Equivalence.thy (
"Some equivalence functions based
on the definition.")
├── Lightweight_Java_Proof.thy (
"A type soundness proof for LJ.")
├── README (
"This file.")
├── ROOT.ML (
"A file directing Isabelle which theories to compile.")
├── config (
"AFP maintenance configuration file.")
├── document
│ ├── root.bib (
"BibTeX bibliography for the 'root.tex'.")
│ └── root.tex (
"LaTeX source for generating the PDF overviewing LJ.")
└── ott-src (
"LJ's Ott source files provided for reference.")
├── Makefile
├── README
├── lj.ott
├── lj.tex
├── lj_base.ott
└── lj_common.ott
Maintaining LJ
--------------
- Lightweight_Java_Definition.thy
Since
"Lightweight_Java_Definition.thy" is generated
by Ott, it should _not_
be modified directly. Please either:
1) E-mail the main author (rok@strnisa.com)
to sort out any problem; or,
2) Modify the provided Ott-source files
to obtain the desired result. Please
notify the main author (rok@strnisa.com) of any such changes.
- Lightweight_Java_Equivalence.thy
and Lightweight_Java_Proof.thy
These two files can be modified at will, as long as the semantics of
"progress"
and "wf_preservation" is preserved.
Suchen
