Programming Notes – Program States, Part 1
Activating a program statement changes the program state to a new state that agrees with an expected result, and a working model of the program state is essential to program statement analysis.
A program state describes the characteristics of each variable. Thus, a program state may be described as a set of ordered n-tuples, where each n-tuple describes a variable. A single n-tuple contains the name, type, value, etc of each variable. For simplicity, the n-tuples for each variable are described as an ordered pair, where the first part of the ordered pair is the name of the variable, and the second part of the ordered pair is the value of the variable.
Suppose that x, y, and z are program variables. Then program state s is described as the set
s = {<’x’,10>,<’y’,15>,<’z’,25>}.
The program state s is also called a point in the program state space. Each ordered pair describing a variable is a dimension in the program state space.
Program state s has many properties. Some of the properties of state s are:
x=10,
x>0,
z=x+y.
Each of the expressions shown above is true in program state s. The following implications are true.
s Þ x=10,
s Þ x>0,
s Þ z=x+y.
The set P = {s|s Þ x=10} contains all program states satisfying the expression x=10. The set P is a program state space. Some members of the set P are:
{<’x’,10>,<’y’,15>,<’z’,25>},
{<’x’,10>,<’y’,25>,<’z’,25>},
{<’x’,10>,<’y’,10>,<’z’,50>}.
Using set notation, the point <x,10> is a member of program state s, and program state s is a member of the states implying expression P. The state space {s} is a subset of the set P.
<’x’,10> Î s
s Î P
{s} Í P.
The symbol P may represent an expression defining a state space or the symbol P may refer to the set directly. When P is an expression, the state space may be represented by the set
{s|P:s}.
In context, the symbol P may also represent the set. In the expression
P = {s|P:s}
the first occurrence of P refers to a set, and the second occurrence of P is an expression.
An expression may contain local variables, program variables, or variables defining points in a state space. There is a class for each type of variable. A program variable belongs to the Prog class and a point in a state space is a variable in the State class. Local variables belong to the Local class. The expression
s Þ z=x+y
contains the state variable s and program variable z, x, and y. The expression does not clarify the type of each variable, so variables may be quantified by the class to which they belong. The expression below is equivalent.
State.s Þ Prog.z= Prog.x + Prog.y
Local variables are used when program variables and state variables are not convenient. Local variables are obvious candidates as quantifying variables.
A specific point in the state space is a point in which all of the program variables are known.
s = {<’x’,10>,<’y’,15>,<’z’,25>}
A point contains a finite set of variables with a value or expression for each variable. Each point in a state space contains the same set of variables. Each variable is distinct, and each point contains the same set of variables. A point p can be defined as
p = {i|0£i£m:<’p.i’, Pp.i>}
p.i refers to the ith variable. ‘p.i’ refers to the name of the ith variable. Pp.i refers to the expressionfor the ith variable.
Let s = {<’x’,10>,<’y’,15>,<’z’,25>}.
Then s.1 = x, s.2 = y, s.3 = z.
Also Ss.1 = 19, Ss.2 = 15, Ss.3 = 25.
Definition 1: Point s = {<’x’,Sx>,<’y’,Sy>,×××,<’z’,Sz>}
Point s = {i|0£i£m:<’s.i’, Ss.i>}
The use of the letter S for each expression does not mean that the same expression applies to each variable. The expression Sx is distinct from the expression Sy.
In Definition 1, Sv is an expression containing a program variable or program variables or constants or both. Generally, the expression Sx is a literal or a simple expression with a value equal to the respective variable. During the process of analyzing different programs, points may contain more complex expressions with a combination of different variables and constants. The point is specific when all of the variables have a defined value. The point is arbitrary when the values of some or all of the variables are not known.
s = {<’x’,x>,<’y’,y>,<’z’,z>}
s = {i|0£i£m:<’s.i’,s.i>}
In a theorem, a reference to an arbitrary point usually refers to the special case when each expression represents the variable, so each variable expression is Sv = v.
Definition 2: s is an arbitrary point º s = {<’x’,x>,<’y’,y>,×××,<’z’,z>}
º s = {i|0£i£m:<’s.i’,s.i>}
In general, a program contains a finite number of variables, and a point in the program state is described by the properties of each program variable.
An expression applies to a point. If the expression is true at the point then the point is in the set defined by the expression. The value of the expression should therefore be derived from the respective values of the variables at the point in question. Expressions are ambiguous if they have variable references that apply to more than one point.
The variables of point s may be shown as a list.
s.var.list = x,y,x,×××
A list may be denoted as a quantified expression in which the items of the list are assigned a unique integer value. The range of integers is defined as a range expression. The variable list may be written with a quantifying variable:
s.var.list = (,i|range:s.i)
Since there are a finite number of variables, the range may be shown as 0£i£m.
If the range denotes an empty range, then the list is empty. The following list is empty,
(,i|0<i<0:s.i)
The expressions of each variable in point s may be shown as a list.
s.expression.list = Sx,Sy,Sz×××
The quantified expression may be used to denote the list of expressions.
(,i|0<i<0:Ss.i)
The value of expression P at point s is shown in Axiom 1. The replacement of the respective variables occurs simultaneously.
The evaluation of an expression at a point requires the simultaneous replacement of all variables in the expression, so that there is no implicit assignment operation in the evaluation process. Nevertheless, partial evaluation is a valuable tool in analyzing substitution patterns. A sequence of substitutions is defined as nested single substitutions. Evaluation means performing the innermost substitution, then performing the next substitution, etc.
Definition 3: P[substitution 1][substitution 2] = (P[substitution
1])[substitution 2]
P[x := E][y :=F] º (P[x := E])[y :=F]
Sequential substitution is not the same as the simultaneous substitution of all program variables. Nonetheless, some sequential substitutions are equivalent to simultaneous substitutions, and evaluation may proceed in a sequential manner. When the expression is the variable; substitution does not change the target expression, and the order of substitution is not important. When the variable is not in the target expression; substitution does not change the target expression, and the order of substitution is not important. When the variable is not in any other substitutable expression and no other variable is in the substitutable expression, then the order of substation is not important.
Axiom 2: Ss.k = s.k Ú (ØOccurs(s.k, P) Ú ("i|0£i£m Ù i¹k: ØOccurs(s.k, Ss.i) Ù ØOccurs(s.i, Ss.k)) Þ
P[s] = P[s.k := Ss.k][(,i|0£i£m Ù i¹k:s.i) := (,i|0£i£mÙi¹k:Ss.i)]
Replacement of a point over a point distributes over the expressions defining the point. Thus
Axiom 3: {<’x’,Sx>,<’y’,Sy>,×××,<’z’,Sz>}[t]
= {<’x’,Sx[t]>,<’y’,Sy[t]>,×××,<’z’,Sz[t]>}
{i|0£i£m:<’s.i’, Ss.i>}[t] = {i|0£i£m:<’s.i’, Ss.i[t]>}
Equality of two points
Two points are equal if all corresponding points are equal. Each point has the same set of variables, so the corresponding variables at each point may be ordered in the same way. Each point is a distinct point, so every expression representing a variable has definite value.
Axiom 4: p=s º ("i|0£i£m:Ss.i = Pp.i)
Substitution of one point in another
A point is an expression that evaluates to the description of a point in which each variable may have a distinct value. So the expression
t[s]
represents the point t substituted by the point s. The expression t[s] may represent a distinct point or a set of points depending on the resulting expressions of each variable in t[s]. If each variable has a distinct value, then the point is distinct. If one or more variables is an expression with imbedded variables, then the expression t[s] may represent a set of points. Let P be an expression that denotes set P. P[t] represents the new expression with the values of each variable in P replaced by the values of the corresponding variables at point t. Similarly, P[t[s]] represents the new expression with the values of each variable in P replaced by the values of the corresponding variables at point t[s]. Because t and s are both points in the program state space, each point has the same set of variables, so substitution is associative.
Axiom 5: P[t[s]] = P[t][s]
Evaluation of P[t][s] follows the normal order of innermost substitution first as described in definition 3; (P[t])[s].
Evaluation of one point against another point is the same as collectively evaluating each variable expression against the point.
Theorem 1:s[t] = {i|0£i£m:<’s.i’,Ss.i[t]>}
A point expression contains a reference to each variable in the program, so every point contains the same set of variables.
An expression that evaluates to true or false is a logical predicate. A logical predicate may be used to define a set of points in a state space, and membership of a point in a state space depends on the evaluation of the expression defining the state space at the point in question.
An arbitrary point has characteristics appropriate to Axiom 2, making sequential substitution of arbitrary point variables possible.
If s is an arbitrary point then any predicate is equivalent to the predicate at the point. With arbitrary points, variable replacements do not change the predicate.
Theorem 2: s is an arbitrary point Þ P = P[s]
As in the arbitrary point theorem, arbitrary variables may be omitted from the substitution rule.
Theorem 3: P[<’x’,E>,(,i|1£i£m:<’s.i’,s.i>)] = P[x := E]
The same concept is true for specific points in which the content of the variables is known.
Theorem 4: s Î P º P[s]
The expression ‘x’ has a point-wise replacement value equal to the value of x at the point.
Theorem 5: Let x be a program variable.
x[t] = Tx
The following two theorems evaluate the point of a point when one of the points is an arbitrary point. In both cases, an arbitrary point acts as an identity point with respect to the replacement operation.
Theorem 6: Let t be a point, and let s be an arbitrary point.
t[s] = t
Theorem 7: Let t be a point, and let s be an arbitrary point.
s[t] = t
Universal Set of Discourse
The set of all possible program states is the universal set of discourse U. The logical constant true corresponds to the universal set of discourse U. If an expression is always true, then the expression applies to all program states.
Null Set
The logical constant false refers to the condition that no program state is valid. The logical constant false corresponds to the null set Æ.
The set where all points calculate to true represents the Universal set. The set where all points calculate to false represents the null set.
Theorem 8: U = {s|true:s}
Theorem 9: Æ = {s|false:s}
The value of P[s]
The predicate P[s] can be evaluated true or false after the free variables in P are replaced by their respective values.
If there are free variables in P after all substitutions have been made, then the truth-value of predicate P depends on the value of the free variables, and the membership of s in P is not certain.
Let s be the program state
s = {<’x’,10>,<’y’,15>,<’z’,25>}.
Let P = {p|2x < z:p}
Verify whether s Î P.
P[s] = (2x < z)[x,y,z := 10,15,25]
P[s] = (2(10) < 25)
P[s] = (20 < 25)
P[s] = True
s Î P
Let Q = {q|xy is odd:q}
Verify whether s Î Q.
Q[s] = (xy is odd)[x,y,z := 10,15,25]
Q[s] = (10(15) is odd)
Q[s] = (150 is odd)
Q[s] = False
s Ï Q
The Black Box Property occurs when one cannot determine the value of one or more variables in a program state. When a variable is not known, determining whether a state is in a state space may not be possible.
Let t be the state expression
t = {<’x’,10>,<’y’,y>,<’z’,25>}.
The expression for state t does not represent a distinct state, because the value of the program variable y is unknown, so the notion that state t is a member of a state space is inexact at best. Nevertheless, programmers often make decisions with partial information.
Let R = {p|2x < y:p}
Verify whether t Î R.
R[t] = (2x < y)[x,y,z := 10,y,25]
R[t] = (2(10) < y)
R[t] = (20 < y)
The state space t is a member of R only when the value of the variable y is greater than 20. Since the value of y is not known, the membership of t cannot be determined.
The following two examples show cases where one can determine the membership of a state in a state space even if some variables are not known.
Let P = {p|2x < z:p}
Verify whether t Î P.
P[t] = (2x < z)[x,y,z := 10,y,25]
P[t] = (2(10) < 25)
P[t] = (20 < 25)
P[t] = True
t Î P
Let Q = {q|xy is odd:q}
Verify whether t Î Q.
Q[t] = (xy is odd)[x,y,z := 10,y,25]
Q[t] = (10(y) is odd)
Q[t] = ((2)(5)(y) is odd)
Q[t] = False
s Ï Q
Let s be the program state
s = {<’x’,10>,<’y’,15>,<’z’,25>}.
1. Verify if s Î P = {u|z= 2y – 5:u}.
2. Verify if s Î P = {u|x – y is positive:u}.
Provide narratives that explain the meaning of each problem shown above.
Let t be the state
t = {<’x’,10>,<’y’,y>,<’z’,25>}.
3. Verify if t Î P = {u|z= 2y – 5:u}
4. Verify if t Î P = {u|x – y is positive:u}
5. Verify if t Î P = {u|z= 2x + 5:u}
Provide narratives that explain the meaning of each problem shown above.
The points r, s, and t have the values:
r = {<’x’,x-y>,<’y’,y>}
s = {<’x’,x>,<’y’,y+x>}
t = {<’x’,y-x>,<’y’,y>}
The space P is defined by the expression:
P º (x = 3 Ù y = 7)
6. Derive (((P[t])[s])[r])
7. Derive P[t[s[r]]]
Explain why the derived expressions in problems 6 and 7 are the same.
Theorem 3 asserts that set membership is equivalent to evaluating the predicate representing the set at the point of the member, so set operators can be verified by evaluating the predicates at particular points.
P Í Q º ("x|:xÎPÞxÎQ)
º(Theorem 3)
P Í Q º ("x|:P[x]Þ Q[x])
Let P = {s|x×y ³ 12}
Determine if the following sets are subsets of P, supersets of P, or neither
{s|x ³ 6 Ù y ³ 3:s}
{s|x×y ³ 6:s}
{s|x+y ³ 144:s}
Which of the following sets represent the null set?
{s|odd numbers divisible by 2:s}
{s|even numbers divisible by 3:s}
{s|x < 2 Ú x > 2:s}
{s|x < 2 Ù x > 2:s}
Which of the following points are equal?
p = {<’x’,5>,<’y’, ¾>}
q = {<{<’x’,5>,<’y’, .75>}
r = {<{<’x’,1/3>,<’y’, 2>}
s = {<{<’x’,.33>,<’y’, 2>}
t = {<{<’x’,.33>,<’y’, 5-3>}
References:
Dijkstra, Edsgar, 1976, A Discipline of Programming, Englewood Cliffs, NJ: Prentice-Hall
Ganong, Rick 1999, Course notes and comments from M1090 and M2090 math and logic courses, http://www.math.yorku.ca/Who/Faculty/Ganong
Gries, David and Schneider, Fred B., 1993, A Logical Approach to Discrete Math, New York, NY: Springer-Verlag