Function expression state with parent stack: parent_stack arguments: arg_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 parent stack: parent_stack arguments: arg_stack values: value_stack line: line tab: tab
Input:
Output:
Conditional properties that reference this function:
if the following are true:
- expression state at time t = "call_build_args"
- Parameters List at time t = [ ]
then stack at time (t + 1) = [ program context with variables: (Variables Map at time t) and expression state: (expression state with parent stack: (parent stack at time t) arguments: (arguments 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), 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
- stack at time t = [ program context with variables: varis and expression state: (expression state with parent stack: parent_stack arguments: arg_stack values: value_stack line: line tab: tab) and control map: control_map, rest ]
- expression state at time t = "end_expr"
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 j =
return rex
- stack at time t = [ program context with variables: varis and expression state: (expression state with parent stack: parent_stack arguments: arg_stack values: value_stack line: line tab: tab) and control map: control_map, rest ]
- expression state at time t = "end_expr"
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
- stack at time t = [ program context with variables: varis and expression state: (expression state with parent stack: parent_stack arguments: arg_stack values: value_stack line: line tab: tab) and control map: control_map, rest ]
- expression state at time t = "end_expr"
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
- stack at time t = [ program context with variables: varis and expression state: (expression state with parent stack: parent_stack arguments: arg_stack values: value_stack line: line tab: tab) and control map: control_map, rest ]
- expression state at time t = "end_expr"
then expression state at time (t + 1) = "call_returned"
(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
- stack at time t = [ program context with variables: varis and expression state: (expression state with parent stack: parent_stack arguments: arg_stack values: value_stack line: line tab: tab) and control map: control_map, rest ]
- expression state at time t = "end_expr"
then parent stack at time (t + 1) = parent_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
- stack at time t = [ program context with variables: varis and expression state: (expression state with parent stack: parent_stack arguments: arg_stack values: value_stack line: line tab: tab) and control map: control_map, rest ]
- expression state at time t = "end_expr"
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
- stack at time t = [ program context with variables: varis and expression state: (expression state with parent stack: parent_stack arguments: arg_stack values: value_stack line: line tab: tab) and control map: control_map, rest ]
- expression state at time t = "end_expr"
then 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
- stack at time t = [ program context with variables: varis and expression state: (expression state with parent stack: parent_stack arguments: arg_stack values: value_stack line: line tab: tab) and control map: control_map, rest ]
- expression state at time t = "end_expr"
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 j =
return rex
- stack at time t = [ program context with variables: varis and expression state: (expression state with parent stack: parent_stack arguments: arg_stack values: value_stack line: line tab: tab) and control map: control_map, rest ]
- expression state at time t = "end_expr"
then arguments stack at time (t + 1) = arg_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
- stack at time t = [ program context with variables: varis and expression state: (expression state with parent stack: parent_stack arguments: arg_stack values: value_stack line: line tab: tab) and control map: control_map, rest ]
- expression state at time t = "end_expr"
then Return Value at time (t + 1) = Return Value 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 k = s
- k < j
- value at (j - 1) in map (Control Map at time t) = pair ("method", mname)
- stack at time t = [ program context with variables: varis and expression state: (expression state with parent stack: parent_stack arguments: arg_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)
- stack at time t = [ program context with variables: varis and expression state: (expression state with parent stack: parent_stack arguments: arg_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)
- stack at time t = [ program context with variables: varis and expression state: (expression state with parent stack: parent_stack arguments: arg_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)
- stack at time t = [ program context with variables: varis and expression state: (expression state with parent stack: parent_stack arguments: arg_stack values: value_stack line: line tab: tab) and control map: control_map, rest ]
then expression state at time (t + 1) = "call_returned"
(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)
- stack at time t = [ program context with variables: varis and expression state: (expression state with parent stack: parent_stack arguments: arg_stack values: value_stack line: line tab: tab) and control map: control_map, rest ]
then parent stack at time (t + 1) = parent_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)
- stack at time t = [ program context with variables: varis and expression state: (expression state with parent stack: parent_stack arguments: arg_stack values: value_stack line: line tab: tab) and control map: control_map, rest ]
then 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)
- stack at time t = [ program context with variables: varis and expression state: (expression state with parent stack: parent_stack arguments: arg_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)
- stack at time t = [ program context with variables: varis and expression state: (expression state with parent stack: parent_stack arguments: arg_stack values: value_stack line: line tab: tab) and control map: control_map, rest ]
then arguments stack at time (t + 1) = arg_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)
- stack at time t = [ program context with variables: varis and expression state: (expression state with parent stack: parent_stack arguments: arg_stack values: value_stack line: line tab: tab) and control map: control_map, rest ]
then Control Map at time (t + 1) = control_map
(link)
Comments
Please log in to add comments