Home My Page Projects Code Snippets Project Openings diderot
Summary Activity Tracker Tasks SCM

SCM Repository

[diderot] Annotation of /trunk/semantics/semantics
ViewVC logotype

Annotation of /trunk/semantics/semantics

Parent Directory Parent Directory | Revision Log Revision Log


Revision 515 - (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 515
30 : lamonts 489 Values
31 :     v := Num(n) | Bool(b) | String(s) | tensor...??
32 :    
33 : lamonts 490
34 : lamonts 515 /** Strand Enviornment */
35 : lamonts 492 Strand_Status := Active * env | Dead * env | Stablized * env
36 :     env = variable → value
37 : lamonts 515 Strand_Env = Strand_Status * id * commands
38 : lamonts 490
39 : lamonts 492
40 : lamonts 515
41 : lamonts 492 /** Arithmetic & Relational Expressions Evaluation Functions**/
42 : lamonts 490 expr_value = Aexpr * env -> value
43 :     rel_op = Rexpr * env -> value
44 : lamonts 489
45 :    
46 : lamonts 515 Global Enviornment:
47 :     The ∪ character denotes a parallel construct that states that every stand environment
48 :     runs in parallel with each other.
49 : lamonts 492
50 : lamonts 515 ∪ (update(Γ(id),Γ))
51 :    
52 :     id ∈ Strand_env
53 :     Γ = id -> Strand_Env
54 :     dom(Γ) = all active & Stablized strand environments
55 :     newId = Γ * id -> id
56 :    
57 :    
58 :     update: Strand_Env * Γ -> Γ'
59 :     Rules
60 :     (1) -------------------------------------------------------------
61 :     update(((Stabalized,env),id,comm),Γ) ⇓ Γ
62 :    
63 :    
64 :     comm_eval((Active,env),comm,id,Γ) ⇓ (new_status,env',Γ')
65 :     (2) -------------------------------------------------------------------
66 :     update(((Active,env),id,comm),Γ) ⇓ Γ'[(new_status,env')/id]
67 :    
68 :    
69 :    
70 :     comm_eval: Strand_Status * commands * id * Γ -> status * env * Γ'
71 : lamonts 490 Rules
72 : lamonts 492 (1) ------------------------------------------------------
73 : lamonts 515 comm_eval((s, env),stabalize,id,Γ) ⇓ (Stablized,env,Γ)
74 : lamonts 489
75 : lamonts 492
76 :     (2) ------------------------------------------------------
77 : lamonts 515 comm_eval((s, env),die,id,Γ) ⇓ (Dead, env,Γ)
78 : lamonts 489
79 : lamonts 492
80 : lamonts 490 expr_eval(e,env) ⇓ v
81 : lamonts 492 (3) ----------------------------------------------------------
82 : lamonts 515 comm_eval((s,env),x:=e,id,Γ) ⇓ (s,env[x:=v],Γ)
83 : lamonts 490
84 :    
85 : lamonts 515 comm_eval((s, env),c1,Γ) ⇓ (s', env',Γ') comm_eval((s', env),c2,Γ') ⇓ (s'',env'',Γ'')
86 :     (4) ----------------------------------------------------------------------------------------------
87 :     comm_eval((s, env),c1;c2,id,Γ) ⇓ (s', env'',Γ'')
88 : lamonts 490
89 :    
90 : lamonts 515 rel_op(b, env) ⇓ true comm_eval((s, env),c1,id,Γ) ⇓ (s',env',Γ')
91 : lamonts 490 (5) -------------------------------------------------------------------------
92 : lamonts 515 comm_eval((s, env),if b then c1 else c2,id,Γ) ⇓ (s', env',Γ')
93 : lamonts 490
94 : lamonts 492
95 : lamonts 515 rel_op(b,env) ⇓ false comm_eval((s,env),c2,id,Γ) ⇓ (s', env',Γ')
96 : lamonts 492 (6) -------------------------------------------------------------------------
97 : lamonts 515 comm_eval((s, env),if b then c1 else c2,id,Γ) ⇓ (s', env',Γ')
98 : lamonts 492
99 :    
100 : lamonts 515 newId(Γ,id) ⇓ id'
101 :     (7) -----------------------------------------------
102 :     comm_eval((s,env),spawn,id,Γ) ⇓ (s,env,Γ)

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