Scope and type rules for quirk20. [Revision 0]
The judgment
|- S must return
means that the statement S is guaranteed to execute a return
statement.
1 <= i <= n
|- Si must return
----------------------------
|- { D1 ... Dm S1 ... Sn } must return
|- S1 must return
|- S2 must return
---------------------------------
|- if (E) S1 else S2 must return
-------------------------
|- return E; must return
****************************************************************
The types needed for semantic analysis of quirk20 programs are
generated by
T --> VOID | NULL
| BOOLEAN | CHAR | STRING | INT | DOUBLE
| R | T[] | function T (T, ...)
R --> <typeid>
****************************************************************
An abstract data type of type environments is used below to
express the typing rules for quirk20. This ADT is named Tenv,
and is specified as follows.
Signature:
error: -> Tenv
empty: -> Tenv
extend: Tenv x Qsymbol x Qtype x boolean x boolean -> Tenv
extendWithClass: Tenv x Qsymbol x Tenv x Tenv -> Tenv
extendWithTenv: Tenv x Tenv -> Tenv
lookupType: Tenv x Qsymbol -> Qtype
lookupFinal: Tenv x Qsymbol -> boolean
lookupGlobal: Tenv x Qsymbol -> boolean
lookupStatic: Tenv x Qsymbol -> Tenv
lookupDynamic: Tenv x Qsymbol -> Tenv
length: Tenv -> int
identifier: Tenv x int -> Qsymbol
isError: Tenv -> boolean
initial: -> Tenv
Algebraic specification:
extendWithTenv (tenv0, empty())
= tenv0
extendWithTenv (tenv0, extend (tenv1, I1, T, f, g))
= extend (extendWithTenv (tenv0, tenv1), I1, T, f, g)
lookupType (empty(), I1)
= VOID
lookupType (extend (tenv, I1, T, f, g), I1)
= T
lookupType (extend (tenv, I2, T, f, g), I1)
= lookupType (tenv, I1) if I1 != I2
lookupType (extendWithClass(tenv, R, tenv1, tenv2), I1)
= VOID
lookupFinal (empty(), I1)
= true
lookupFinal (extend (tenv, I1, T, f, g), I1)
= f
lookupFinal (extend (tenv, I2, T, f, g), I1)
= lookupFinal (tenv, I1) if I1 != I2
lookupFinal (extendWithClass (tenv, R, tenv1, tenv2), I1)
= true
lookupGlobal (empty(), I1)
= true
lookupGlobal (extend (tenv, I1, T, f, g), I1)
= g
lookupGlobal (extend (tenv, I2, T, f, g), I1)
= lookupGlobal (tenv, I1) if I1 != I2
lookupGlobal (extendWithClass (tenv, R, tenv1, tenv2), I1)
= true
lookupStatic (empty(), I1)
= error()
lookupStatic (extend (tenv, I1, T, f, g), I1)
= error()
lookupStatic (extend (tenv, I2, T, f, g), I1)
= lookupStatic (tenv, I1) if I1 != I2
lookupStatic (extendWithClass (tenv, R1, tenv1, tenv2), R1)
= tenv1
lookupStatic (extendWithClass (tenv, R2, tenv1, tenv2), R1)
= lookupStatic (tenv, I1) if R1 != R2
lookupDynamic (empty(), I1)
= error()
lookupDynamic (extend (tenv, I1, T, f, g), I1)
= error()
lookupDynamic (extend (tenv, I2, T, f, g), I1)
= lookupDynamic (tenv, I1) if I1 != I2
lookupDynamic (extendWithClass (tenv, R1, tenv1, tenv2), R1)
= tenv2
lookupDynamic (extendWithClass (tenv, R2, tenv1, tenv2), R1)
= lookupDynamic (tenv, I1) if R1 != R2
length (empty())
= 0
length (extend (tenv, I1, T, f, g))
= 1 + length (tenv)
length (extendWithClass (tenv, R, tenv1, tenv2))
= 0
identifier (extend (tenv, I1, T, f, g), 0)
= I1
identifier (extend (tenv, I1, T, f, g), n)
= identifier (tenv, n - 1) if n > 0
isError (error()) = true
isError (empty()) = false
isError (extend(_, _, _, _, _)) = false
isError (extendWithClass(_, _, _, _)) = false
initial() is the standard initial environment that contains
bindings for predefined classes and their constants and
methods. This initial environment will be specified
separately, because it is expected to evolve rapidly as the
language develops.
Notation:
tenv[] means tenv.
tenv[I1: T1, ...] means
(extend (tenv, I1, T1, false, false))[...].
****************************************************************
The static local environment of a <classdec> C is static(C),
defined below. The dynamic local environment of a <classdec> C
is dynamic(C), defined below.
The global environment of a quirk20 <program> P is global(P),
which is defined below. The static local environment of a
<classdec> C is static(C). The dynamic local environment of
a <classdec> C is dynamic(C). Both static(C) and dynamic(C)
are defined below.
If the <program> P consists of a single <classdec> C of the form
class R { ... }, then
global(P)
= extendWithClass (initial(), R, static(C), dynamic(C))
If the <program> P has more than one <classdec>, so that it has
the form
class R { ... } P2
where P2 is a program, and
isError (lookupStatic (global(P2), R))
then
global(P)
= extendWithClass (global(P2), R, static(C), dynamic(C))
If C contains no <bodydec>, then
static(C) = dynamic(C) = empty()
Otherwise let D be the first <bodydec> in C, and let tenv1 and
tenv2 be the static and dynamic local environments of the class
obtained from C by deleting its first <bodydec> D.
If D is of the form
<access> constant T I1 = E1;
and lookupType (tenv1, I1) = VOID, then dynamic(C) = tenv2 and
static (C) = extend (tenv1, I1, T, true, true)
If D is of the form
<access> static T I1 = <literal> ;
and lookupType (tenv1, I1) = VOID, then dynamic(C) = tenv2 and
static (C) = extend (tenv1, I1, T, false, true)
If D is of the form
<access> T I1;
and lookupType (tenv2, I1) = VOID, then static(C) = tenv1 and
dynamic (C) = extend (tenv2, I1, T, false, false)
If D is of the form
proc T0 I1 (T1 I1, ..., Tn In) { ... }
and lookupType (tenv1, I1) = VOID, then dynamic(C) = tenv2 and
static (C)
= extend (tenv1, I1, function T0 (T1, ..., Tn), true, true)
****************************************************************
The typing judgment
|- P
means that the <program> contains no scope or type errors.
The typing judgment
tenv |- T
means that, in the type environment tenv, the <type> T contains
no scope or type errors. (In practice, this means that all of
the class names that are mentioned within T are bound to static
and dynamic type environments within tenv.)
The typing judgment
tenv |- C
means that, in the type environment tenv, the <classdec> C
contains no scope or type errors.
The typing judgment
tenv |- D
means that, in the type environment tenv, the <bodydec> or
<localdec> D contains no scope or type errors.
The typing judgment
tenv |- S : T
means that, in the type environment tenv, the <stm> S contains
no scope or type errors and all return statements that it may
execute return a value of type T.
The typing judgment
tenv |- E : T
means that, in the type environment tenv, the expression E has
type T.
The subtyping judgment
tenv |- E <: T
mean that there exists a type T0 such that
tenv |- E : T0
respectively, and T0 is a subtype of T.
T0 is a subtype of T, written T0 <: T, iff one of the following
is true:
1. T0 = T
2. T0 = NULL and T is a <typeid>
3. T = VOID
****************************************************************
The scope and type rules of quirk20 are defined by the following
inference rules. (There are no rules for when statements,
unless statements, for statements, or parenthesized expressions
because the parser translates those constructs into abstract
syntax trees that are handled by the rules below.)
Programs:
for each <classdec> C of P,
global(P) |- C
---------------------------
|- P
Types:
------------
tenv |- void
---------------
tenv |- boolean
------------
tenv |- char
--------------
tenv |- String
-----------
tenv |- int
--------------
tenv |- double
tenv |- T
-----------
tenv |- T[]
tenv |- T0
tenv |- T1
...
tenv |- Tn
-------------------------------------------
tenv |- function (from (T1, ..., Tn) to T0)
false = isError (lookupStatic (tenv, R))
----------------------------------------
tenv |- R
Classes:
tenv1 = extendWithTenv (tenv, lookupStatic (tenv, R))
tenv1 |- D1
...
tenv1 |- Dn
------------------------------------------------------
tenv |- class R { D1 ... Dn }
Class body declarations:
tenv |- T1
tenv |- E1 <: T1
--------------------------------------
tenv |- <access> constant T1 I1 = E1 ;
tenv |- T1
tenv |- E1 <: T1
------------------------------------
tenv |- <access> static T1 I1 = E1 ;
tenv |- T1
------------------------
tenv |- <access> T1 I1 ;
I1 through In are distinct
tenv |- T0
tenv |- T1
...
tenv |- Tn
tenv1 = tenv [I1 : T1, ..., In : Tn]
tenv1 |- S : VOID
---------------------------------------------------
tenv |- <access> proc void I0 (T1 I1, ..., Tn In) S
I1 through In are distinct
tenv |- T0
tenv |- T1
...
tenv |- Tn
tenv1 = tenv [I1 : T1, ..., In : Tn]
|- S must return
tenv1 |- S : T0
-------------------------------------------------
tenv |- <access> proc T0 I0 (T1 I1, ..., Tn In) S
Blocks:
---------------
tenv |- { } : T
tenv |- S1 : T
...
tenv |- Sn : T
----------------------------
tenv |- { S1 S2 ... Sn } : T
tenv |- T1
tenv |- E1 <: T1
tenv1 = tenv [ I1 : T1 ]
tenv1 |- { ... S1 ... Sn } : T
-----------------------------------------
tenv |- { T1 I1 = E1; ... S1 ... Sn } : T
I1 through In are distinct
tenv |- T0
tenv |- T1
...
tenv |- Tn
tenv1 = extend (tenv, I0, function VOID (T1, ..., Tn), true, false)
tenv2 = tenv1 [ I1 : T1, ..., In : Tn ]
tenv2 |- S : VOID
tenv1 |- { ... S1 ... Sn } : T
----------------------------------------------------------------
tenv |- { proc void I0 (T1 I1, ..., Tn In) S ... S1 ... Sn } : T
I1 through In are distinct
|- S must return
tenv |- T0
tenv |- T1
...
tenv |- Tn
tenv1 = extend (tenv, I0, function T0 (T1, ..., Tn), true, false)
tenv2 = tenv1 [ I1 : T1, ..., In : Tn ]
tenv2 |- S : T0
|- S must return
tenv1 |- { ... S1 ... Sn } : T
--------------------------------------------------------------
tenv |- { proc T0 I0 (T1 I1, ..., Tn In) S ... S1 ... Sn } : T
Other statements:
-------------
tenv |- ; : T
tenv |- E : T1
--------------
tenv |- E; : T
tenv |- E : BOOLEAN
tenv |- S1 : T
tenv |- S2 : T
-----------------------------
tenv |- if (E) S1 else S2 : T
tenv |- E : BOOLEAN
tenv |- S1 : T
------------------------
tenv |- while (E) S1 : T
tenv |- E <: T
---------------------
tenv |- return E; : T
Expressions:
false = lookupFinal (tenv, I1)
tenv |- I1 : T1
tenv |- E1 <: T1
------------------------------
tenv |- I1 = E1 : VOID
tenv |- R
tenv0 = lookupStatic (tenv, R)
false = lookupFinal (tenv0, I1)
tenv0 |- I1 : T1
tenv |- E1 <: T1
-------------------------------
tenv |- R.I1 = E1 : VOID
tenv |- E0 : R
tenv0 = lookupDynamic (tenv, R)
false = lookupFinal (tenv0, I1)
tenv0 |- I1 : T1
tenv |- E1 <: T1
--------------------------------
tenv |- E0.I1 = E1 : VOID
tenv |- E1 : T1[]
tenv |- E2 : int
tenv |- E3 <: T1
-----------------------------
tenv |- E1 [ E2 ] = E3 : VOID
B is || or &&
tenv |- E1 : BOOLEAN
tenv |- E2 : BOOLEAN
-------------------------
tenv |- E1 B E2 : BOOLEAN
B is one of the following binary operations:
== !=
tenv |- E1 : BOOLEAN
tenv |- E2 : BOOLEAN
--------------------------------------------
tenv |- E1 B E2 : BOOLEAN
B is one of the following binary operations:
== !=
tenv |- E1 : CHAR
tenv |- E2 : CHAR
--------------------------------------------
tenv |- E1 B E2 : BOOLEAN
B is one of the following binary operations:
== != < <= > >=
tenv |- E1 : STRING
tenv |- E2 : STRING
--------------------------------------------
tenv |- E1 B E2 : BOOLEAN
B is one of the following binary operations:
== != < <= > >=
tenv |- E1 : INT
tenv |- E2 : INT
--------------------------------------------
tenv |- E1 B E2 : BOOLEAN
B is one of the following binary operations:
== != < <= > >=
tenv |- E1 : DOUBLE
tenv |- E2 : DOUBLE
--------------------------------------------
tenv |- E1 B E2 : BOOLEAN
B is one of the following binary operations:
== !=
T is a <typeid> or the NULL type
tenv |- E1 <: T
tenv |- E2 <: T
--------------------------------------------
tenv |- E1 B E2 : BOOLEAN
B is one of the following binary operations:
+
tenv |- E1 : STRING
tenv |- E2 : STRING
--------------------------------------------
tenv |- E1 B E2 : STRING
B is one of the following binary operations:
+ - * /
tenv |- E1 : INT
tenv |- E2 : INT
--------------------------------------------
tenv |- E1 B E2 : INT
B is one of the following binary operations:
+ - * /
tenv |- E1 : DOUBLE
tenv |- E2 : DOUBLE
------------------------
tenv |- E1 B E2 : DOUBLE
tenv |- E1 : BOOLEAN
----------------------
tenv |- ! E1 : BOOLEAN
tenv |- E1 : INT
------------------
tenv |- - E1 : INT
tenv |- E1 : DOUBLE
---------------------
tenv |- - E1 : DOUBLE
-------------------
tenv |- null : NULL
----------------------
tenv |- true : BOOLEAN
-----------------------
tenv |- false : BOOLEAN
L is a charliteral
------------------
tenv |- L : CHAR
L is a Stringliteral
--------------------
tenv |- L : STRING
L is an intliteral
------------------
tenv |- L : INT
L is a floatliteral
-------------------
tenv |- L : DOUBLE
tenv |- R
--------------------
tenv |- new R () : R
tenv |- T
tenv |- E : INT
-------------------------
tenv |- new T [ E ] : T[]
tenv |- R
tenv0 = lookupStatic (tenv, R)
tenv0 |- I1 : T1
------------------------------
tenv |- R.I1 : T1
tenv |- E0 : function T0 (T1, ..., Tn)
tenv |- E1 <: T1
...
tenv |- En <: Tn
--------------------------------------
tenv |- E0 (E1, ..., En) : T0
T1 = lookupType (tenv, I1)
VOID != T1
--------------------------
tenv |- I1 : T1
tenv |- E : R
tenv0 = lookupDynamic (tenv, R)
tenv0 |- I1 : T1
-------------------------------
tenv |- E.I1 : T1
tenv |- E1 : T[]
tenv |- E2 : INT
---------------------
tenv |- E1 [ E2 ] : T