# HG changeset patch # User oheimb # Date 981400455 -3600 # Node ID cc421547e744d2eef2e6135af8b0768350c33a30 # Parent 4f6fd393713fa079e8fbd31a8d298cfea28d7ac0 improved document (added headers etc) diff -r 4f6fd393713f -r cc421547e744 src/HOL/MicroJava/J/Conform.thy --- a/src/HOL/MicroJava/J/Conform.thy Mon Feb 05 14:59:44 2001 +0100 +++ b/src/HOL/MicroJava/J/Conform.thy Mon Feb 05 20:14:15 2001 +0100 @@ -2,9 +2,9 @@ ID: $Id$ Author: David von Oheimb Copyright 1999 Technische Universitaet Muenchen +*) -Conformity relations for type safety of Java -*) +header "Conformity Relations for Type Soundness Proof" theory Conform = State + WellType: diff -r 4f6fd393713f -r cc421547e744 src/HOL/MicroJava/J/Decl.thy --- a/src/HOL/MicroJava/J/Decl.thy Mon Feb 05 14:59:44 2001 +0100 +++ b/src/HOL/MicroJava/J/Decl.thy Mon Feb 05 20:14:15 2001 +0100 @@ -2,9 +2,9 @@ ID: $Id$ Author: David von Oheimb Copyright 1997 Technische Universitaet Muenchen +*) -Class declarations and programs -*) +header "Class Declarations and whole Programs" theory Decl = Type: diff -r 4f6fd393713f -r cc421547e744 src/HOL/MicroJava/J/Eval.thy --- a/src/HOL/MicroJava/J/Eval.thy Mon Feb 05 14:59:44 2001 +0100 +++ b/src/HOL/MicroJava/J/Eval.thy Mon Feb 05 20:14:15 2001 +0100 @@ -2,10 +2,9 @@ ID: $Id$ Author: David von Oheimb Copyright 1999 Technische Universitaet Muenchen +*) -Operational evaluation (big-step) semantics of the -execution of Java expressions and statements -*) +header "Operational Evaluation (big-step) Semantics" theory Eval = State + WellType: diff -r 4f6fd393713f -r cc421547e744 src/HOL/MicroJava/J/Example.thy --- a/src/HOL/MicroJava/J/Example.thy Mon Feb 05 14:59:44 2001 +0100 +++ b/src/HOL/MicroJava/J/Example.thy Mon Feb 05 20:14:15 2001 +0100 @@ -2,14 +2,22 @@ ID: $Id$ Author: David von Oheimb Copyright 1997 Technische Universitaet Muenchen +*) -The following example Bali program includes: +header "Example MicroJava Program" + +theory Example = Eval: + +text {* +The following example MicroJava program includes: class declarations with inheritance, hiding of fields, and overriding of methods (with refined result type), instance creation, local assignment, sequential composition, method call with dynamic binding, literal values, - expression statement, local access, type cast, field assignment (in part), skip + expression statement, local access, type cast, field assignment (in part), + skip. +\begin{verbatim} class Base { boolean vee; Base foo(Base x) {return x;} @@ -26,9 +34,8 @@ e.foo(null); } } -*) - -theory Example = Eval: +\end{verbatim} +*} datatype cnam_ = Base_ | Ext_ datatype vnam_ = vee_ | x_ | e_ diff -r 4f6fd393713f -r cc421547e744 src/HOL/MicroJava/J/JBasis.thy --- a/src/HOL/MicroJava/J/JBasis.thy Mon Feb 05 14:59:44 2001 +0100 +++ b/src/HOL/MicroJava/J/JBasis.thy Mon Feb 05 20:14:15 2001 +0100 @@ -2,9 +2,9 @@ ID: $Id$ Author: David von Oheimb Copyright 1999 TU Muenchen +*) -Some auxiliary definitions. -*) +header "Some Auxiliary Definitions" theory JBasis = Main: @@ -14,8 +14,8 @@ constdefs - unique :: "('a \\ 'b) list => bool" - "unique == nodups \\ map fst" + unique :: "('a \ 'b) list => bool" + "unique == nodups \ map fst" lemma fst_in_set_lemma [rule_format (no_asm)]: @@ -55,7 +55,7 @@ done lemma Ball_set_table_: - "(\\(x,y)\\set l. P x y) --> (\\x. \\y. map_of l x = Some y --> P x y)" + "(\(x,y)\set l. P x y) --> (\x. \y. map_of l x = Some y --> P x y)" apply(induct_tac "l") apply(simp_all (no_asm)) apply safe diff -r 4f6fd393713f -r cc421547e744 src/HOL/MicroJava/J/JTypeSafe.thy --- a/src/HOL/MicroJava/J/JTypeSafe.thy Mon Feb 05 14:59:44 2001 +0100 +++ b/src/HOL/MicroJava/J/JTypeSafe.thy Mon Feb 05 20:14:15 2001 +0100 @@ -2,9 +2,9 @@ ID: $Id$ Author: David von Oheimb Copyright 1999 Technische Universitaet Muenchen +*) -Type Safety Proof for MicroJava -*) +header "Type Safety Proof" theory JTypeSafe = Eval + Conform: @@ -280,7 +280,7 @@ apply( fast intro: hext_trans) apply( simp) apply( drule eval_no_xcpt) -apply( erule FAss_type_sound, simp (no_asm) (*###rule refl*), assumption+) +apply( erule FAss_type_sound, rule HOL.refl, assumption+) apply( tactic prune_params_tac) (* Level 52 *) diff -r 4f6fd393713f -r cc421547e744 src/HOL/MicroJava/J/State.thy --- a/src/HOL/MicroJava/J/State.thy Mon Feb 05 14:59:44 2001 +0100 +++ b/src/HOL/MicroJava/J/State.thy Mon Feb 05 20:14:15 2001 +0100 @@ -2,9 +2,9 @@ ID: $Id$ Author: David von Oheimb Copyright 1999 Technische Universitaet Muenchen +*) -State for evaluation of Java expressions and statements -*) +header "Program State" theory State = TypeRel + Value: diff -r 4f6fd393713f -r cc421547e744 src/HOL/MicroJava/J/Term.thy --- a/src/HOL/MicroJava/J/Term.thy Mon Feb 05 14:59:44 2001 +0100 +++ b/src/HOL/MicroJava/J/Term.thy Mon Feb 05 20:14:15 2001 +0100 @@ -2,9 +2,9 @@ ID: $Id$ Author: David von Oheimb Copyright 1999 Technische Universitaet Muenchen +*) -Java expressions and statements -*) +header "Expressions and Statements" theory Term = Value: diff -r 4f6fd393713f -r cc421547e744 src/HOL/MicroJava/J/Type.thy --- a/src/HOL/MicroJava/J/Type.thy Mon Feb 05 14:59:44 2001 +0100 +++ b/src/HOL/MicroJava/J/Type.thy Mon Feb 05 20:14:15 2001 +0100 @@ -2,9 +2,9 @@ ID: $Id$ Author: David von Oheimb Copyright 1999 Technische Universitaet Muenchen +*) -Java types -*) +header "Java types" theory Type = JBasis: diff -r 4f6fd393713f -r cc421547e744 src/HOL/MicroJava/J/TypeRel.thy --- a/src/HOL/MicroJava/J/TypeRel.thy Mon Feb 05 14:59:44 2001 +0100 +++ b/src/HOL/MicroJava/J/TypeRel.thy Mon Feb 05 20:14:15 2001 +0100 @@ -2,9 +2,9 @@ ID: $Id$ Author: David von Oheimb Copyright 1999 Technische Universitaet Muenchen +*) -The relations between Java types -*) +header "Relations between Java Types" theory TypeRel = Decl: diff -r 4f6fd393713f -r cc421547e744 src/HOL/MicroJava/J/Value.thy --- a/src/HOL/MicroJava/J/Value.thy Mon Feb 05 14:59:44 2001 +0100 +++ b/src/HOL/MicroJava/J/Value.thy Mon Feb 05 20:14:15 2001 +0100 @@ -2,9 +2,9 @@ ID: $Id$ Author: David von Oheimb Copyright 1999 Technische Universitaet Muenchen +*) -Java values -*) +header "Java Values" theory Value = Type: diff -r 4f6fd393713f -r cc421547e744 src/HOL/MicroJava/J/WellForm.thy --- a/src/HOL/MicroJava/J/WellForm.thy Mon Feb 05 14:59:44 2001 +0100 +++ b/src/HOL/MicroJava/J/WellForm.thy Mon Feb 05 20:14:15 2001 +0100 @@ -2,20 +2,28 @@ ID: $Id$ Author: David von Oheimb Copyright 1999 Technische Universitaet Muenchen - -Well-formedness of Java programs -for static checks on expressions and statements, see WellType.thy +*) -improvements over Java Specification 1.0 (cf. 8.4.6.3, 8.4.6.4, 9.4.1): -* a method implementing or overwriting another method may have a result type - that widens to the result type of the other method (instead of identical type) - -simplifications: -* for uniformity, Object is assumed to be declared like any other class -*) +header "Well-formedness of Java programs" theory WellForm = TypeRel: +text {* +for static checks on expressions and statements, see WellType. + +\begin{description} +\item[improvements over Java Specification 1.0 (cf. 8.4.6.3, 8.4.6.4, 9.4.1):]\ \\ +\begin{itemize} +\item a method implementing or overwriting another method may have a result type +that widens to the result type of the other method (instead of identical type) +\end{itemize} + +\item[simplifications:]\ \\ +\begin{itemize} +\item for uniformity, Object is assumed to be declared like any other class +\end{itemize} +\end{description} +*} types 'c wf_mb = "'c prog => cname => 'c mdecl => bool" constdefs diff -r 4f6fd393713f -r cc421547e744 src/HOL/MicroJava/J/WellType.thy --- a/src/HOL/MicroJava/J/WellType.thy Mon Feb 05 14:59:44 2001 +0100 +++ b/src/HOL/MicroJava/J/WellType.thy Mon Feb 05 20:14:15 2001 +0100 @@ -2,21 +2,25 @@ ID: $Id$ Author: David von Oheimb Copyright 1999 Technische Universitaet Muenchen +*) -Well-typedness of Java programs +header "Well-typedness Constraints" +theory WellType = Term + WellForm: + +text {* the formulation of well-typedness of method calls given below (as well as the Java Specification 1.0) is a little too restrictive: Is does not allow methods of class Object to be called upon references of interface type. -simplifications: -* the type rules include all static checks on expressions and statements, e.g. - definedness of names (of parameters, locals, fields, methods) - -*) - -theory WellType = Term + WellForm: - +\begin{description} +\item[simplifications:]\ \\ +\begin{itemize} +\item the type rules include all static checks on expressions and statements, + e.g.\ definedness of names (of parameters, locals, fields, methods) +\end{itemize} +\end{description} +*} types lenv (* local variables, including method parameters and This *) = "vname \ ty" 'c env diff -r 4f6fd393713f -r cc421547e744 src/HOL/MicroJava/ROOT.ML --- a/src/HOL/MicroJava/ROOT.ML Mon Feb 05 14:59:44 2001 +0100 +++ b/src/HOL/MicroJava/ROOT.ML Mon Feb 05 20:14:15 2001 +0100 @@ -1,4 +1,3 @@ - goals_limit := 1; add_path "J";