Function 'while stack' at time s

the 'while stack' tracks the state of 'while' loops at time s

Format:

'while stack' at time s

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 j = a class named name with bases: bases

  then 'while stack' at time (t + 1) = 'while 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 k = s
  • k < j
  • value at (j - 1) in map (Control Map at time t) = pair ("class", class_name)

  then 'while stack' at time (t + 1) = 'while 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 = a method named method_name with parameters params

  then 'while stack' at time (t + 1) = 'while 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 = for target in iterable:
  • Expression Stack at time t = [ [ ], [ ] ]

  then 'while stack' at time (t + 1) = 'while stack' at time t

  (link)

• if the following are true:

  • the line at time t = i
  • the tab at time t = j
  • number of lines = i - 1
  • value at (j - 1) in map (Control Map at time t) = trio ("for", for_line, iterable)

  then 'while stack' at time (t + 1) = 'while 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 = x = c

  then 'while stack' at time (t + 1) = 'while 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 = if test:

  then 'while stack' at time (t + 1) = 'while 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 = elif test:

  then 'while stack' at time (t + 1) = 'while 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 = else:

  then 'while stack' at time (t + 1) = 'while 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 = "while" statement with condition (function call with name: name and arguments: args)

  then 'while stack' at time (t + 1) = 'while 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 = continue

  then 'while stack' at time (t + 1) = 'while 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 = function definition where name: name and parameters: params

  then 'while stack' at time (t + 1) = 'while 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 v

  then 'while stack' at time (t + 1) = 'while 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 = Python list elements

  then 'while stack' at time (t + 1) = 'while 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 = obj_name.method_name(args)
  • expression state at time t = "not_expr"

  then 'while stack' at time (t + 1) = 'while 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 = assign statement with target target and expression (obj_name.method_name(args))
  • expression state at time t = "not_expr"

  then 'while stack' at time (t + 1) = 'while 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 = obj."append"(el)

  then 'while stack' at time (t + 1) = 'while 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 = a class named name with bases: bases

  then 'while stack' at time (t + 1) = 'while 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 k = s
  • k < j
  • value at (j - 1) in map (Control Map at time t) = pair ("class", class_name)

  then 'while stack' at time (t + 1) = 'while 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 = a method named method_name with parameters params

  then 'while stack' at time (t + 1) = 'while 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 = obj.key = value

  then 'while stack' at time (t + 1) = 'while 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 = x.y = z
  • expression state at time t = "end_expr"

  then 'while stack' at time (t + 1) = 'while 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 k = s
  • k < j
  • value at (j - 1) in map (Control Map at time t) = pair ("method", method_name)

  then 'while stack' at time (t + 1) = 'while 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 = for target in iterable:
  • iterable is a variable

  then 'while stack' at time (t + 1) = 'while 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 = for target in iterable:
  • expression state at time t = "end_expr"

  then 'while stack' at time (t + 1) = 'while 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 = for target in iterable_ex:
  • value at j in map (Control Map at time t) = trio ("for", i, [ elem, rest ])

  then 'while stack' at time (t + 1) = 'while 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 = for target in iterable_ex:
  • value at j in map (Control Map at time t) = trio ("for", i, [ ])

  then 'while stack' at time (t + 1) = 'while 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 k = s
  • k < j
  • value at (j - 1) in map (Control Map at time t) = trio ("for", for_line, iterable)

  then 'while stack' at time (t + 1) = 'while stack' at time t

  (link)

• if the following are true:

  • the line at time t = i
  • the tab at time t = j
  • number of lines = i - 1
  • value at (j - 1) in map (Control Map at time t) = trio ("for", for_line, iterable)

  then 'while stack' at time (t + 1) = 'while stack' at time t

  (link)

Comments

Please log in to add comments