Inf / AWL

AWL: Abstract W Language

Notes feb18

do we need language and/xor byte code
exceptions with resume?
extensions
- compiling or currying (compiletime features)
- oo
- environment? 4 d-Registers: callFrame, obj, class, sys
- multiprocessing ... / operating system
  - wie funktionieren interrupts: Exceptions? spontaneous calls? messages?

Differences to AsmL, Lit.Lit#Gur00

strictly sequential, no parallel updateset
less typing: function do not have an arity, they just take 0-n arguments
code is contained in the universe - do we need better syntax for (nested) preprocessor capabilities?

Notation

S^* for a Set S: the set of finite sequences from S. We often will use [], the sequence of length 0

the starting Point

a set C of constants C ⊇ {true, false, value, key, size, undef, noexpr, nobool, 0, 1, ...} including a sufficiently large prefix of the naturals (for the tupels in the program)
a set V ⊇ (C ∪ {cf}) the Vocabulary including the Constants and (time dependent) function cf for the current frame
E the expressions over V - i.e. all the programms using the Vocabulary V
I the object Identifiers a set big enough for any program, disjoint from any other set used here
U ⊇ (C ∪ I ∪ E) the Universe (i.e. the base set of the model)
a Model is an interpretation of the Elements of the Vocabulary as partial functions U^* → U. The special value undef is thrown if the program accesses an undefined location
M: (cf → I) ∪ (I → U^* → U): The time dependet (Memory) State of a computation: the current frame is an object and each object is a partial Map from U^* to U

Abstract syntax of AWL

Variant with 3 - clarified

A program is simply an expression. E ist the set of all expressions. Given a Vocabulary V, E are the expressions, formed by a finite many application of the following recursive definition of an expression e ∈ E

abstract syntax of e	e is any of the following
syntactical definitions
e	designates an expression
u	an element from the universe
v	an element from the vocabulary
loc = e [ e ]	an location in a map for access or update
v \| v( e* )	evaluation of a function from the vocabulary
u	a constant (for internal use in the compiler)
new	creation of a new, empty map
loc	access to the value at a location of an objectMap, throw undef if not defined
loc := e	update (or add) the value at a location of an objectMap and return new value for
loc :-	remove the location from the map return old value or throw undefined
for loc in e do e	process each defined location in the range of a map, by assigning each key to cf[e]
e ; e	sequential composition
while e do e	loop in sequential composition
if e then e else e	if statement: choose one
fun e	function definition for later execution
e ( ( e := e )* )	call of the function in the first expression with a new frame with the given mappings
return e	return from a call
throw e	throw an exception
try e catch loc handle e	catch exceptions

concrete syntax

expression begin
- string, number ==> constant values in u
- name ==> v if defined else ==> cf.name
- .? ==> cf[?]
vocabulary und call syntax gleich ==> implementierung ohne code change
- zurzeit vocabluary nur unbenannte args, call nur benannte!

Variant with 2 - clarified

abstract syntax of e	e is any of the following
syntactical definitions
e	designates an expression
al = e := e (, e := e)*	assignment list
u	an element from the universe
v	an element from the vocabulary
v \| v() \| v( e (, e)* )	evaluation of a function from the vocabulary
const u	a constant (for internal use in the compiler)
new	creation of a new, empty map
e [ e ]	access to the value at a location of an objectMap, throw undef if not defined
e [ al ]	update (or add) the value at a location of an objectMap and return new value
e [ e :- ]	remove a location from an objectMap and return old value, throw undef if not defined
for e (=> e)? in e do e	process each defined location in the range of a map, by assigning each key to cf[e]
e ; e	sequential composition
while e do e	loop in sequential composition
if e then e else e	if statement: choose one
fun e	function definition for later execution
det e	evaluate e at declaration time: evaluate e and assign the result to a const, if the det nesting level reaches the fun nesting level
exe e	evalute the expression if it yields an expression execute it, otherwise throw noCode
e ( al )	call of the function in the first expression with a new frame with the given mappings
return e	return from a call
throw e	throw an exception
try e catch e handle e	catch exceptions

Variant with 1-dimensinal maps and as few iterations as possible

abstract syntax of e	e is any of the following
syntactical definitions
e	designates an expression
l = e [ e ]	(update) location: point in the range of an objectMap
u	an element from the universe
v	an element from the vocabulary
v \| v() \| v( e (, e)* )	evaluation of a function from the vocabulary
const u	a constant (for internal use in the compiler)
new	creation of a new, empty map
l	access to the value at a location of an objectMap, throw undef if not defined
l := e	update (or add) the value at a location of an objectMap and return new value
remove l	remove a location from an objectMap and return old value, throw undef if not defined
all l in e do e	process each defined location in the range a map, by assigning each key to l
e ; e	sequential composition
while e do e	loop in sequential composition
if e then e else e	if statement: choose one
fun e	function definition for later execution
call e with e	call of the function in the first expression with the frame in the second
return e	return from a call
exe e	evaluate e and assign the result to a const, if the exe nesting level reaches call nesting level
throw e	throw an exception
try e catch l by e	catch exceptions

ass = e [ a1? (, a1?)* ]
a1 = e (:- | :-- | ( ( := | :== | :=+) e)?

Variant with mulitdimensional maps and iterations

A program is simple an expression. E ist the set of all expressions. Given a Vocabulary V, E are the expressions, formed by a finite many application of the following recursive definition of an expression e ∈ E

abstract syntax of e	e is any of the following
syntactical definitions
e	designates an expression
e = e*	designates a finite sequence of expressions, possibly of length 0
r = e	point in the range of an objectMap
l = e[ r ]	(update) location: point in the range of an objectMap
if = if e then e (elif e then e)* else e	if statement
v(e)	evaluation of a function from the vocabulary
new (r := e)*	creation of a new object with initialisation
l	access to the value at a location of an objectMap, throw undef if not defined
l := e	update (or add) the value at a location of an objectMap and return new value
remove l	remove a location from an objectMap and return old value, throw undef if not defined
all e in e do e	process each defined location in the range an object, by updating the fields value, (key, size), (key, 1) ... in the object of the first expression for the evaluation of the last expression
e ; e	sequential composition
while e do e	loop in sequential composition
if	if statement: choose one
fun e	function definition for later execution
call e (r := e)*	call of a function
return e	return from a call
throw e	throw an exception
try e catch l if	catch exceptions

Operational Semantics

The evalution of an expression updates the current state and returns a value, thus we model it by a function S

S: M × E → M × {normal, return, throw} × U

The middle element say, whether the result has been generated by normal program flow, a return or a throw. We define S recursively.

helper functions

FN((m₁, f₁, u₁), ..., (m_n, f_n, u_n)) := (m_k, f_k, u_k)
- with k ∈ {1..n} and (k = n or f_k <> normal) and ∀ j<k: f_j = normal
FE(m, e) = FN(
- (m₀, f₀) = (m, normal)
- , (m_i, f_i, u₁, ..., u_i) with (m_i, f_i, u_i)= S(m_i-1, e_i) for n >= i > 0
- ) with n = length(e)
FE(m₀, e₁, ..., e_h) (m_{k', k″}, f_{k', k″}, u_{1, 1}, ..., u_{k', k″})
- multiple e_i are iterated anlogously
FF(m, k, e₁, ... e_i) = FF'(m, 1, e₁, ... e_i) with FF'(m, k, e₁, ... e_i)
- = if f' <> normal then (m', f', u')
- elif u' = true then (m', f', k)
- elif u' <> false then (m', throw, nobool)
- elif i=1 then (m', f', k+1)
- else FF'(m', k+1, e₂, ... e_i)
- with (m', f', u') = S(m, e₁)
S(m, v(e)) = if f' <> normal then (m', f', u_k) elif v(u₁, ... u_n) is defined then (m″, normal, v(u₁, ... u_n)) else (m', throw, undef) with
- (m', f', u₁, ..., u_k) = FE(m, e)
S(m, e'[e]) = if f_k <> normal then (m_k, f_k, u_k) elif m_n(u', u₁, ... u_n) is defined then (m_n, normal,m_n(, u', u₁, ... u_n)) else (m_n, throw, undef) with
- (m', f', u') = S(m, e')
- (n, k, m_k, f_k, u₁, ..., u_k) = if f' <> normal then (length(e), 0, m', f', u') else FE(m', e)
S(m, e'[e] := e″) = if f″ <> normal then (m″, f″, u″) else (m'″, normal, u″) with
- (n, k, m_k, f_k, u₁, ..., u_k) as above
- (m″, f″, u″) = if f_k <> normal then (m_k, f_k, u_k) else S(m_n, e″)
- m″' = m″ except m'″(e', u₁, ..., u_n) = u″
S(m, call e e′₁ = e₁, ..., e′_k = e_k) = FN(
- (m₁, f₁, u₁) = S(m, e)
- , if u₁ ∉ E then (m₁, throw, noexpr)
- , (m₂, f₂, u₂) = S(m₁, new e′₁ = e₁, ..., e′_k = e_k)
- , (m₃, f₂, u₂) with m₃ = m₂ except m₃(cf) = u₂
- , (m₄, f₄, u₄) with (m₄, g₄, u₄) = S(m₃, u₁) and f₄ = if g₄ = return then normal else g₄
- , (m₅, f₄, u₄) with m₅ = m₄ except m₅(cf) = m(cf)
- )
S(m, all e' in e″ do e) = FN(
- (m', f', u') = S(m, e')
- , (m₀, f₀, u₀) = S(m', e″)
- , ...
- , (m_i-1, f_i-1, u_i-1)
- , (m'_i, f_i-1, u_i-1) with m'_i = m_i-1 except m'_i(u', key, size) = size(t_i), m'_i(u', key, k) = t_i,k for k=1..size(t_i) and m'_i(u', value) = m_i-1(u₀, t_i) for a tuple t_i ∈ U^*
- , (m_i, f_i, u_i) = S(m'_i, e)
- , ...
- , (m_j, f_j, u_j)
- ) such that all the t_i are different and ∩(range(e″ in m_i)) ⊆ {t₁, ..., t_j} ⊆ ∪(range(e″ in m_i))
S(m, try e catch e'[e″] if e₁ then e'₁ elif e₂ then e'₂ ... else e'_i)
- = if f₁ <> throw then (m₁, f₁, u₁) = S(m, e)
- elif f₂ <> normal then (m₂, f₂, u₂) = S(m₁, e'[e″] := u₁)
- elif f₃ <> normal then (m₃, f₃, j) = FF(m₂, e₁, ..., e_i-1)
- elif e'_j is missing in syntax then (m₃, f₁, u₁)
- else S(m₃, e'_j)