LARA

Differences

This shows you the differences between two versions of the page.

Link to this comparison view

Both sides previous revision Previous revision
Next revision
Previous revision
Next revision Both sides next revision
sav07_lecture_20 [2007/06/05 19:03]
kremena.diatchka
sav07_lecture_20 [2007/06/05 19:22]
vkuncak
Line 44: Line 44:
   - must follow protocol: ​ (open (read+write)* close)*   - must follow protocol: ​ (open (read+write)* close)*
   - must follow protocol: (startLog stopLog)*   - must follow protocol: (startLog stopLog)*
 +
 +
  
  
Line 54: Line 56:
 Let $S$ be the set of program states and $V$ be the set of vertices in the control flow graph. Then we can describe a point in the program as: Let $S$ be the set of program states and $V$ be the set of vertices in the control flow graph. Then we can describe a point in the program as:
  
-$(s,c)$+$(c,s)$
  
-where $\in S\in V$+where $\in V\in S$
  
  
Line 67: Line 69:
 Then we can formally define the semantics of a big step ($\mapsto$) as: Then we can formally define the semantics of a big step ($\mapsto$) as:
  
-$(c_{0},s_{1}) \mapsto (c_{3}, s_{2})$ ​+$(c_{1},s_{1}) \mapsto (c_{2}, s_{2})$ ​
  
 where $(s_{1},​s_{2}) \in r$ iff $(c_{0},​s_{1}) \rightarrow (c_{3},​s_{2})$ where $(s_{1},​s_{2}) \in r$ iff $(c_{0},​s_{1}) \rightarrow (c_{3},​s_{2})$
Line 92: Line 94:
 $(s, l, c, t)$ $(s, l, c, t)$
  
-Here $l \in L$, where $L$ is the set of local variables of a procedure. Everything would be popped off from $l$ when the procedure returns control to the callee.+Here $l \in L$, where $L$ is the set of mappings ​of local variables of a procedure ​to their values. ​ Furthermore,​ on each procedure call, the program pushes $l$ on the stack along with the program point Everything would be popped off from $l$ when the procedure returns control to the callee.
  
 One instance where small step semantics would be necessary is in concurrency,​ so that we can take into account interleaving. ​ One instance where small step semantics would be necessary is in concurrency,​ so that we can take into account interleaving. ​