Beispiel


[Erweiterung : Scheifen] ... [Index]
Nun folgt die Definition einer einfachen denotationellen Semantik, mit der es möglich ist einfache Programme abzubilden und semantisch auszuwerten. Was im Anschluß an die Definition beispielhaft geschehen soll.

Syntactic Domains

P:program
L:list
S:statement
E:expression
N:number
D:digit
I:identifier
L:letter

P -> L
L -> L1 ';' L2 | S
S -> I ':=' E | 'if' E 'then' L1 'else' L2 'fi' | 'while' E 'do' L 'od'
E -> E1 '+' E2 | E1 '-' E2 | E1 '*' E2 | E1 '/' E2 | E1 '%' E2 | N
N -> N D | D
D -> '0' | '1' | '2' | ... | '9'
I -> I L | L
L -> 'a' | 'b' | 'c' | ... | 'z'

Semantic Domains

Domäne v: Integer = {..., -2, -1, 0, 1, 2, ...}
Operationen
+:Integer x Integer->Integer
-:Integer x Integer->Integer
*:Integer x Integer->Integer
/:Integer x Integer->Integer
%:Integer x Integer->Integer

Domäne Env: Environment = Identifier -> Integer_

Semantic Functions

P : Program -> Environment_
P[[L]] = L[[L]](Env0)
L : list -> Environment_ -> Environment_
L[[L1 ';' L2]](Env) = L[[L2]](Env) o L[[L1]](Env)
L[[S]] = S[[S]]
S : Statement -> Environment_ -> Environment_
S[[I ':=' E]](Env) = Env & {I = E[[E]](Env)}
S[['if' E 'then' L1 'else' L2 'fi']](Env) = cond(E[[E]](Env);L[[L1]](Env);L[[L2]](Env))
S[['while' E 'do' L 'od']](Env) = cond(E[[E]](Env);L[[L]](Env) o S[['while' E 'do' L 'od']](Env);id(Env))
E : Expression -> Environment_ -> Integer_
E[[E1 '+' E2]](Env) = E[[E1]](Env) + E[[E2]](Env)
E[[E1 '-' E2]](Env) = E[[E1]](Env) - E[[E2]](Env)
E[[E1 '*' E2]](Env) = E[[E1]](Env) * E[[E2]](Env)
E[[E1 '/' E2]](Env) = E[[E1]](Env) / E[[E2]](Env)
E[[E1 '%' E2]](Env) = E[[E1]](Env) % E[[E2]](Env)
E[[I]](Env) = Env(I)
E[[N]](Env) = N[[N]]
N : Number -> Integer
N[[ND]] = 10 * N[[N]] + N[[D]]
N[[D]] = D[[D]]
D : Digit -> Integer
D[['0']] = 0
D[['1']] = 1
D[['2']] = 2
D[['3']] = 3
D[['4']] = 4
D[['5']] = 5
D[['6']] = 6
D[['7']] = 7
D[['8']] = 8
D[['9']] = 9

Beispiel 1 : Stelle des höchstwertigen Bits

      ret := 0;
      members := members / 2;
      while members do
         members := members / 2;
         ret := ret + 1
      od

Initialzustand
Env { members = 16

(L[['while' members 'do' members ':=' members '/' 2 ';' ret ':=' ret '+' 1 'od']] o L[[members ':=' members '/' 2]] o L[[ret ':=' 0]])(Env) =
S[['while' members 'do' members ':=' members '/' 2 ';' ret ':=' ret '+' 1 'od']](S[[members ':=' members '/' 2]](S[[ret ':=' 0]])) =
S[['while' members 'do' members ':=' members '/' 2 ';' ret ':=' ret '+' 1 'od']](S[[members ':=' members '/' 2]](Env & {ret = E[[0]]})) =
S[['while' members 'do' members ':=' members '/' 2 ';' ret ':=' ret '+' 1 'od']](S[[members ':=' members '/' 2]](Env & {ret = 0})) =
S[['while' members 'do' members ':=' members '/' 2 ';' ret ':=' ret '+' 1 'od']](Env & {members = E[[members '/' 2]](Env)}) =
S[['while' members 'do' members ':=' members '/' 2 ';' ret ':=' ret '+' 1 'od']](Env & {members = 8}) =
cond(E[[members]];(S[['while' members 'do' members ':=' members '/' 2 ';' ret ':=' ret '+' 1 'od']] o S[[ret ':=' ret '+' 1]] o S[[members ':=' members '/' 2]])(Env);id(Env)) =
cond(8;(S[['while' members 'do' members ':=' members '/' 2 ';' ret ':=' ret '+' 1 'od']] o S[[ret ':=' ret '+' 1]] o S[[members ':=' members '/' 2]])(Env);id(Env)) =
cond(4;(S[['while' members 'do' members ':=' members '/' 2 ';' ret ':=' ret '+' 1 'od']] o S[[ret ':=' ret '+' 1]] o S[[members ':=' members '/' 2]])(Env);id(Env)) =
cond(2;(S[['while' members 'do' members ':=' members '/' 2 ';' ret ':=' ret '+' 1 'od']] o S[[ret ':=' ret '+' 1]] o S[[members ':=' members '/' 2]])(Env);id(Env)) =
cond(1;(S[['while' members 'do' members ':=' members '/' 2 ';' ret ':=' ret '+' 1 'od']] o S[[ret ':=' ret '+' 1]] o S[[members ':=' members '/' 2]])(Env);id(Env)) =
cond(0;(S[['while' members 'do' members ':=' members '/' 2 ';' ret ':=' ret '+' 1 'od']] o S[[ret ':=' ret '+' 1]] o S[[members ':=' members '/' 2]])(Env);id(Env)) =
id(Env) =
Env

Env { members = 0
ret = 4

[Zurück] ... [Nach oben] ...