| author | wenzelm |
| Fri, 01 Sep 2000 19:40:57 +0200 | |
| changeset 9793 | 2c3d4e03e00c |
| parent 9348 | f495dba0cb07 |
| child 10042 | 7164dc0d24d8 |
| permissions | -rw-r--r-- |
| 8011 | 1 |
(* Title: HOL/MicroJava/J/Term.thy |
2 |
ID: $Id$ |
|
3 |
Author: David von Oheimb |
|
4 |
Copyright 1999 Technische Universitaet Muenchen |
|
5 |
||
6 |
Java expressions and statements |
|
7 |
*) |
|
8 |
||
|
9346
297dcbf64526
re-structuring MicroJava; added Example; corrected := syntax; simplfied cast
oheimb
parents:
9240
diff
changeset
|
9 |
Term = Value + |
| 8011 | 10 |
|
| 9240 | 11 |
datatype binop = Eq | Add (* function codes for binary operation *) |
12 |
||
| 8011 | 13 |
datatype expr |
14 |
= NewC cname (* class instance creation *) |
|
| 9348 | 15 |
| Cast cname expr (* type cast *) |
| 8011 | 16 |
| Lit val (* literal value, also references *) |
| 9240 | 17 |
| BinOp binop expr expr (* binary operation *) |
| 8011 | 18 |
| LAcc vname (* local (incl. parameter) access *) |
19 |
| LAss vname expr (* local assign *) ("_\\<Colon>=_" [ 90,90]90)
|
|
20 |
| FAcc cname expr vname (* field access *) ("{_}_.._"[10,90,99 ]90)
|
|
21 |
| FAss cname expr vname |
|
|
9346
297dcbf64526
re-structuring MicroJava; added Example; corrected := syntax; simplfied cast
oheimb
parents:
9240
diff
changeset
|
22 |
expr (* field ass. *)("{_}_.._:=_"[10,90,99,90]90)
|
| 8011 | 23 |
| Call expr mname (ty list) (expr list)(* method call*) |
24 |
("_.._'({_}_')" [90,99,10,10] 90)
|
|
25 |
and stmt |
|
26 |
= Skip (* empty statement *) |
|
27 |
| Expr expr (* expression statement *) |
|
28 |
| Comp stmt stmt ("_;; _" [ 61,60]60)
|
|
29 |
| Cond expr stmt stmt ("If'(_') _ Else _" [ 80,79,79]70)
|
|
30 |
| Loop expr stmt ("While'(_') _" [ 80,79]70)
|
|
31 |
end |