Function expression state with expression stack: expr_stack values: value_stack line: line tab: tab
the expression state (expr_state) stores information needed to continue expression evaluation after a child expression is computed, including the various stacks and the location (line and tab) of the expression
Format:
expression state with expression stack: expr_stack values: value_stack line: line tab: tab
Input:
Output:
Conditional properties that reference this function:
if the following are true:
- the line at time t = i
- the tab at time t = j
- statement at line i, tab k = s
- k < j
- value at (j - 1) in map (Control Map at time t) = pair ("method", mname)
- Context Stack at time t = [ program context with variables: varis and expression state: (expression state with expression stack: expr_stack values: value_stack line: line tab: tab) and control map: control_map, rest ]
then Variables Map at time (t + 1) = varis
(link)if the following are true:
- the line at time t = i
- the tab at time t = j
- statement at line i, tab k = s
- k < j
- value at (j - 1) in map (Control Map at time t) = pair ("method", mname)
- Context Stack at time t = [ program context with variables: varis and expression state: (expression state with expression stack: expr_stack values: value_stack line: line tab: tab) and control map: control_map, rest ]
then the line at time (t + 1) = line
(link)if the following are true:
- the line at time t = i
- the tab at time t = j
- statement at line i, tab k = s
- k < j
- value at (j - 1) in map (Control Map at time t) = pair ("method", mname)
- Context Stack at time t = [ program context with variables: varis and expression state: (expression state with expression stack: expr_stack values: value_stack line: line tab: tab) and control map: control_map, rest ]
then the tab at time (t + 1) = tab
(link)if the following are true:
- the line at time t = i
- the tab at time t = j
- statement at line i, tab k = s
- k < j
- value at (j - 1) in map (Control Map at time t) = pair ("method", mname)
- Context Stack at time t = [ program context with variables: varis and expression state: (expression state with expression stack: expr_stack values: value_stack line: line tab: tab) and control map: control_map, rest ]
then Expression Stack at time (t + 1) = expr_stack
(link)if the following are true:
- the line at time t = i
- the tab at time t = j
- statement at line i, tab k = s
- k < j
- value at (j - 1) in map (Control Map at time t) = pair ("method", mname)
- Context Stack at time t = [ program context with variables: varis and expression state: (expression state with expression stack: expr_stack values: value_stack line: line tab: tab) and control map: control_map, rest ]
then Context Stack at time (t + 1) = rest
(link)if the following are true:
- the line at time t = i
- the tab at time t = j
- statement at line i, tab k = s
- k < j
- value at (j - 1) in map (Control Map at time t) = pair ("method", mname)
- Context Stack at time t = [ program context with variables: varis and expression state: (expression state with expression stack: expr_stack values: value_stack line: line tab: tab) and control map: control_map, rest ]
then Value Stack at time (t + 1) = value_stack
(link)if the following are true:
- the line at time t = i
- the tab at time t = j
- statement at line i, tab k = s
- k < j
- value at (j - 1) in map (Control Map at time t) = pair ("method", mname)
- Context Stack at time t = [ program context with variables: varis and expression state: (expression state with expression stack: expr_stack values: value_stack line: line tab: tab) and control map: control_map, rest ]
then Control Map at time (t + 1) = control_map
(link)if Parameters List at time t = [ ], then Context Stack at time (t + 1) = [ program context with variables: (Variables Map at time t) and expression state: (expression state with expression stack: (Expression Stack at time t) values: (Value Stack at time t) line: (the line at time t) tab: (the tab at time t)) and control map: (Control Map at time t), Context Stack at time t ]
(link)if the following are true:
- the line at time t = i
- the tab at time t = j
- statement at line i, tab j =
return rex
- Context Stack at time t = [ program context with variables: vars and expression state: (expression state with expression stack: expr_stack values: value_stack line: line tab: tab) and control map: control_map, rest ]
- Expression Stack at time t = [ [ ], [ ] ]
then Variables Map at time (t + 1) = vars
(link)if the following are true:
- the line at time t = i
- the tab at time t = j
- statement at line i, tab j =
return rex
- Context Stack at time t = [ program context with variables: vars and expression state: (expression state with expression stack: expr_stack values: value_stack line: line tab: tab) and control map: control_map, rest ]
- Expression Stack at time t = [ [ ], [ ] ]
then the line at time (t + 1) = line
(link)if the following are true:
- the line at time t = i
- the tab at time t = j
- statement at line i, tab j =
return rex
- Context Stack at time t = [ program context with variables: vars and expression state: (expression state with expression stack: expr_stack values: value_stack line: line tab: tab) and control map: control_map, rest ]
- Expression Stack at time t = [ [ ], [ ] ]
then the tab at time (t + 1) = tab
(link)if the following are true:
- the line at time t = i
- the tab at time t = j
- statement at line i, tab j =
return rex
- Context Stack at time t = [ program context with variables: vars and expression state: (expression state with expression stack: expr_stack values: value_stack line: line tab: tab) and control map: control_map, rest ]
- Expression Stack at time t = [ [ ], [ ] ]
then Control Map at time (t + 1) = control_map
(link)if the following are true:
- the line at time t = i
- the tab at time t = j
- statement at line i, tab j =
return rex
- Context Stack at time t = [ program context with variables: vars and expression state: (expression state with expression stack: expr_stack values: value_stack line: line tab: tab) and control map: control_map, rest ]
- Expression Stack at time t = [ [ ], [ ] ]
then Context Stack at time (t + 1) = rest
(link)if the following are true:
- the line at time t = i
- the tab at time t = j
- statement at line i, tab j =
return rex
- Context Stack at time t = [ program context with variables: vars and expression state: (expression state with expression stack: expr_stack values: value_stack line: line tab: tab) and control map: control_map, rest ]
- Expression Stack at time t = [ [ ], [ ] ]
then Expression Stack at time (t + 1) = expr_stack
(link)if the following are true:
- the line at time t = i
- the tab at time t = j
- statement at line i, tab j =
return rex
- Context Stack at time t = [ program context with variables: vars and expression state: (expression state with expression stack: expr_stack values: value_stack line: line tab: tab) and control map: control_map, rest ]
- Expression Stack at time t = [ [ ], [ ] ]
then Value Stack at time (t + 1) = value_stack
(link)
Comments
Please log in to add comments