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 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