Decl.thy

(*  Title:      isabelle/Bali/Decl.thy
    ID:         $Id: Decl.thy,v 1.2 1997/10/22 12:00:05 oheimb Exp $
    Author:     David von Oheimb
    Copyright   1997 Technische Universitaet Muenchen

The type system of Java: Field, method, interface, and class declarations 

simplifications:
* no field modifiers yet, i.e. every field is public, non-static, non-final

* no method modifiers yet, i.e. every method is public, non-static, non-final
* result statement replaced by result expression (evaluated at the end of the
  execution of the body; transformation is always possible (with goto, while)
* a void method is replaced by one that returns Unit of dummy type Void
* no local variables; may be simulated with additional parameter
* each method has exactly one (explicit) parameter; this may be an object with
  as many fields as required if the method has more than one parameter

* no interface modifiers yet, i.e. every interface is public
* no interface fields yet[, no ambiguous fields allowed]

* no class modifiers yet, i.e. every class is public, non-final
* every class except Object has an explicit superclass
* each class implements at most one interface; multiple implementation
  may be simulated with an intermediate interface extending all the others
* [no ambiguous class fields allowed]
* Object does not have any standard methods

*)

Decl = Term +

types	field
	= "ty"

        fdecl		(* field declaration, cf. 8.3 (, 9.3) *)
	= "ename * field"


types	sig		(* signature of a method, cf. 8.4.2 *)
	= "mname * ty"

	mhead		(* method head (excluding signature) *)
	= "ty"
	(* result type *)

	mbody		(* method body *)
	= "stmt * expr"
	(* block, result expression *)
	
	methd		(* method in a class *)
	= "mhead * mbody"

	mdecl		(* method declaration in a class *)
	= "sig * methd"

types	iface		(* interface *)
	= "tname list * (sig * mhead) list"
	(* superinterface list, methods *)

	idecl		(* interface declaration, cf. 9.1 *)
	= "tname * iface"

types	class		(* class *)
	= "tname option * tname option * fdecl list * mdecl list"
	(* superclass, implemented interface, fields, methods*)

	cdecl		(* class declaration, cf. 8.1 *)
	= "tname * class"

consts

  Object  :: tname	(* name of root class *)
  ObjectC :: cdecl	(* decl of root class *)

defs 

 ObjectC_def "ObjectC == (Object, (None, None, [], []))"

end