AlgolSemantics

Aenderungen:

in U noch Referenzen R aufnehmen (i, name) geschützt und Prozeduren P (i?, code) geschützt. Referenz, Value und Name? Parameter
- resolveRef(a, n) = with v=s.a.n: if v = undef then err elsif v ∈ U then (a, n) elif v ∈ R resolveRef(v_a, v_n) elsif v ∈ P then whith q = functionCallv)....
  - shift
Mit DatenTypen: Strukturen aufnehmen, wasserdichter Schutz für R und P
CodeFile

Semantics of Algol Blocks

U = Universum = alle Values ⊇ Nat disjointUnion {new, old, undef, void, err}

N = alle Names disjointUnion {hist, lex, ll}

F = Funktionen a set of functions f: U* → U

axiom: ∀ f ∈ F, if x ∈ {new, old, undef, err} then f(..., x, ...) = err

state s: Nat → {new, old, N → U}

axiom: ∃ s_last ∈ Nat: s.i = new ⇔ i > s_last

def s_cur = {i ∈ Nat | s.i ∉ {new, old} and ∀j > i: s.i ∈ {new, old}}

hist

s.0.hist = undef

∀ i ∈ [1 .. s_last]: s.i.hist ∈ [0 .. i-1]

lex

s.0.lex = undef

∀ i ∈ [1 .. s_last]: s.i.lex ∈ [0 .. i-1]

def ll

s.0.ll = 0

∀ i ∈ [1 .. s_last]: s.i.ll = 1 + s.(s.i.lex).ll

Dynamics

E = statements and expression e: State x E → State x Flow x U. The evaluation of a statment in state s yields a (possibly) modified state and a value from the universe, it yields void if no value is generated. Flow = {cont, return, throw, err} determines the flow of excecution. We define the valid programs

explicit lexical reference lll: State x Nat x Nat → err ∪ Nat:

lll(s, i, l) := if i = s.i.ll then i elif l > s.i.ll then err else lll(s, s.i.lex, l)

implicit lexical reference lln: State x Nat x N → err ∪ Nat:

lln(s, i, n) := if s.i.n ≠ undef then i elif s.i.lex = undef then err else lln(s, s.i.lex, n)

expr := u | n | l n | f expr* | ass | call | return

u ∈ U. A constant from the Univers:

e(s, u) := (s, cont, u)

a name n ∈ N is evaluated to its value in the current block or a lexical ancestor:

r = lln(s, s_cur, n)

e(s, n) = (s, if r = undef then err else cont, r)

a lexically qualified name (l, n) ∈ Nat x N is evaluated to its value in the block of the lexical level l of the current lexical chain:

r = lll(s, s_cur, l)

e(s, l n) = (s, if r = undef then err else r, r)

f ∈ F a function evaluation, if number and type of parameters is correct, otherwise it raises an error. e(s, f(e₁, ..., e_k)) is defined by;

's₀ := s; f'_0_ = cont

∀ i ∈ [1..k]: (s_i, f_i, p_i) := if f_i-1 = cont then e(s_i-1, e_i) else (s_i-1, f_i-1, p_i-1)

r := f(p₁, ..., p_k)

e(s, f(e₁, ..., e_k)) := if f_k ≠ cont then (s_k, f_k, p_k) elif r = err then (s_k, err, 'badCall') else (s_k, cont, r)

note that for k=0 f is a constant and both definitions yield the same.

ass := n e' | l n e': An assignment changes a single variable if it is defined to the the evalution of the expression e'. if the variable is undefined an error is raised. e(s, ass n e') is defined by:

notDef := lln(s, s_cur, n) = undef

(s', f', r') := if notDef then (s, err, 'undefined') else (s", cont, r') with s" = s' modifiedBy s".lln(s, s_cur, n).n := r'

e(s, ass l n e') is defined similarly with lll instead of lln.

call := l q (n expr)* n*: calls a procedure with statements q, parameter (n expr) * and local variables n*. e(s, call l q n₁ e₁ ...n_k e_k l₁ ... l_m) is defined by

s₀ := s; f₀ = cont

∀ i ∈ [1..k]: (s_i, f_i, p_i) := if f_i-1 = cont then e(s_i-1, e_i) else (s_i-1, f_i-1, p_i-1)

s' = s_k modifiedBy s'.(1+s'_k.last) = (hist := s'_k.cur, lex := l, n₁ := p₁, ..., n_k := p_k, l₁ := null, ..., l_m := null, everywhereElse := undef)

(s", f", r") := if f_k = cont then e(s', q) else (s_k, f_k, p_k)

assert s_cur = s"_cur

return := return (void | expr): returns from the current procedure call with the given expression or void. The excecution of the currentCodeBlock ends with an executed return statement and the program continues with the codeBlock from s.s_cur.hist. e(s, return e') is defined by:

(s', f', r') := e(s, e')

s" = s' modifiedBy s".s'_cur = old

e(s, return e') := if f' = ret then (s", cont, r') elif f' = cont then (s", err, 'noReturn') else (s", f', r')

assert s.s_cur.hist = s"_cur

is defined by lln or lll respectively as in expr name or l name. call (n expr)* n* | return expr