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 Both sides next revision
sav07_lecture_20 [2007/06/05 19:06]
kremena.diatchka old revision restored
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 93: 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. ​