Annotation of /trunk/semantics/semantics

Parent Directory | Revision Log

---

Revision 492 - (view) (download)

1 :	lamonts	489	Diderot Formal Semantics
2 :			===============================
3 :
4 :			variable ::= string
5 :			id ::= integer
6 :
7 :			Arithmetic expression (Aexp)
8 :	lamonts	492	e ::= n for n ∈ R
9 :	lamonts	489	| x for x = variable
10 :			| e1 + e2 for e1,e2 ∈ Aexp, Aexp
11 :			| e1 - e2 for e1,e2 ∈ Aexp, Aexp
12 :			| e1 * e2 for e1,e2 ∈ Aexp, Aexp
13 :			| e1 / e2 for e1,e2 ∈ Aexp, Aexp
14 :
15 :			Relational expression (Rexp)
16 :	lamonts	492	b ::= true
17 :			| false
18 :	lamonts	489	| e1 == e2 for e1,e2 ∈ Aexp, Aexp
19 :	lamonts	490	| e1 < e2 for e1,e2 ∈ Aexp, Aexp
20 :			| e1 > e2 for e1,e2 ∈ Aexp, Aexp
21 :	lamonts	489	| e1 <= e2 for e1,e2 ∈ Aexp, Aexp
22 :			| e1 >= e2 for e1,e2 ∈ Aexp, Aexp
23 :
24 :			Commands (Comm)
25 :	lamonts	492	c ::= x := e for x = variable, e ∈ Aexp
26 :			| c1; c2 for c1,c2 ∈ Comm
27 :			| if b then c1 else c2 for c1,c2 ∈ Comm and b ∈ Rexp
28 :			| stabalize
29 :	lamonts	489
30 :	lamonts	490
31 :	lamonts	489	Values
32 :			v := Num(n) | Bool(b) | String(s) | tensor...??
33 :
34 :	lamonts	490
35 :	lamonts	492	Strand_Status := Active * env | Dead * env | Stablized * env
36 :			env = variable → value
37 :	lamonts	490
38 :	lamonts	492	/** Global Environment Functions **/
39 :	lamonts	489	Strand_Env = Strand_Status * id * commands * env
40 :	lamonts	492	Γ = id -> Strand_Env dom(Γ) = all Active & Stablized Strand Environments
41 :			newId = Γ * id -> id
42 :
43 :			/** Arithmetic & Relational Expressions Evaluation Functions**/
44 :	lamonts	490	expr_value = Aexpr * env -> value
45 :			rel_op = Rexpr * env -> value
46 :	lamonts	489
47 :
48 :	lamonts	492	comm_eval: Strand_Status * commands -> status * env
49 :
50 :	lamonts	490	Rules
51 :	lamonts	492	(1) ------------------------------------------------------
52 :			comm_eval((s, env),stabalize) ⇓ (Stablized, env)
53 :	lamonts	489
54 :	lamonts	492
55 :			(2) ------------------------------------------------------
56 :			comm_eval((s, env),die) ⇓ (Dead, env)
57 :	lamonts	489
58 :	lamonts	492
59 :	lamonts	490	expr_eval(e,env) ⇓ v
60 :	lamonts	492	(3) ----------------------------------------------------------
61 :			comm_eval((s,env),x:=e) ⇓ (s,env[x:=v])
62 :	lamonts	490
63 :
64 :	lamonts	492	comm_eval((s, env),c1) ⇓ (s', env') comm_eval((s', env),c2) ⇓ (s'',env'')
65 :			(4) ---------------------------------------------------------------------------------------
66 :			comm_eval((s, env),c1;c2) ⇓ (s', env'')
67 :	lamonts	490
68 :
69 :	lamonts	492	rel_op(b, env) ⇓ true comm_eval((s, env),c1) ⇓ (s',env')
70 :	lamonts	490	(5) -------------------------------------------------------------------------
71 :	lamonts	492	comm_eval((s, env),if b then c1 else c2) ⇓ (s', env')
72 :	lamonts	490
73 :	lamonts	492
74 :			rel_op(b,env) ⇓ false comm_eval((s,env),c2) ⇓ (s', env')
75 :			(6) -------------------------------------------------------------------------
76 :			comm_eval((s, env),if b then c1 else c2) ⇓ (s', env')
77 :
78 :
79 :
80 :	lamonts	490	update: Strand_Env -> Strand_Env
81 :			Rules
82 :	lamonts	492
83 :	lamonts	489	(1) -------------------------------------------------------------
84 :	lamonts	492	update(((Stabalized,env),id,comm>)) ⇓ ((Stabalized,env),id,comm)
85 :	lamonts	489
86 :
87 :	lamonts	492	comm_eval((Active,env),comm) ⇓ (new_status,env')
88 :			(2) -------------------------------------------------------------
89 :			Update(((Active,env),_,comm>)) ⇓ ((new_status,env'),id,comm)
90 :	lamonts	489

---

root@smlnj-gforge.cs.uchicago.edu	ViewVC Help
Powered by ViewVC 1.0.0