- English only

# Lab for Automated Reasoning and Analysis LARA

# Differences

This shows you the differences between two versions of the page.

sav08:relational_semantics [2009/05/26 12:54] vkuncak |
sav08:relational_semantics [2015/04/21 17:30] (current) |
||
---|---|---|---|

Line 13: | Line 13: | ||

A pair of integers $(v,v')$ is in relation, written $(v,v') \in r_1$, if and only if $v' = v + 1$. Using set comprehensions, we write | A pair of integers $(v,v')$ is in relation, written $(v,v') \in r_1$, if and only if $v' = v + 1$. Using set comprehensions, we write | ||

- | \[ | + | \begin{equation*} |

r_1 = \{(v,v') \mid v'=v+1 \} | r_1 = \{(v,v') \mid v'=v+1 \} | ||

- | \] | + | \end{equation*} |

The meaning $r_2$ of | The meaning $r_2$ of | ||

x = x + x | x = x + x | ||

is | is | ||

- | \[ | + | \begin{equation*} |

r_2 = \{ (v,v') \mid v' = 2v \} | r_2 = \{ (v,v') \mid v' = 2v \} | ||

- | \] | + | \end{equation*} |

The meaning of | The meaning of | ||

Line 39: | Line 39: | ||

Our programs can have any finite number of integer variables. Let $V$ denote the set of variable names such as 'x' in the example above. The state of our program is a function $V \to R$ mapping variable names to their values, and the set of states | Our programs can have any finite number of integer variables. Let $V$ denote the set of variable names such as 'x' in the example above. The state of our program is a function $V \to R$ mapping variable names to their values, and the set of states | ||

- | \[ | + | \begin{equation*} |

S = (V \to R) | S = (V \to R) | ||

- | \] | + | \end{equation*} |

is the set of all such functions. We assume that the range of variables is $R = \mathbb{Z}$ (the set of integers), but most of what we say will be independent on whether the variables are integers or have some other type. | is the set of all such functions. We assume that the range of variables is $R = \mathbb{Z}$ (the set of integers), but most of what we say will be independent on whether the variables are integers or have some other type. | ||

In the above increment program, $V = \{"x"\}$ and a state is of the form $\{("x",v)\}$ for some integer $v$ (recall that we represent each function $x$ as relation $\{(x,f(x)\mid x \in D \}$). So the increment function is given by a relation, call it $r$, that takes the state $\{("x",v)\}$ and maps it to state $\{("x",v+1)\}$: | In the above increment program, $V = \{"x"\}$ and a state is of the form $\{("x",v)\}$ for some integer $v$ (recall that we represent each function $x$ as relation $\{(x,f(x)\mid x \in D \}$). So the increment function is given by a relation, call it $r$, that takes the state $\{("x",v)\}$ and maps it to state $\{("x",v+1)\}$: | ||

- | \[ | + | \begin{equation*} |

r = \{(\{("x",v)\}, \{("x",v')\}) \mid v' = v + 1 \} | r = \{(\{("x",v)\}, \{("x",v')\}) \mid v' = v + 1 \} | ||

- | \] | + | \end{equation*} |

What happens when we have more than one variable? Let $V = \{"x", "y"\}$ and consider this program: | What happens when we have more than one variable? Let $V = \{"x", "y"\}$ and consider this program: | ||

x = y + y | x = y + y | ||

The meaning of this program is given by relation | The meaning of this program is given by relation | ||

- | \[ | + | \begin{equation*} |

r = \{(\{("x",v),("y",u)\},\{("x",v'),("y",u')\}) \mid v'=2u \land u' = u \} | r = \{(\{("x",v),("y",u)\},\{("x",v'),("y",u')\}) \mid v'=2u \land u' = u \} | ||

- | \] | + | \end{equation*} |

Renaming variables so the initial value of variable "x" is denoted $x$ and final value denoted $x'$, we have | Renaming variables so the initial value of variable "x" is denoted $x$ and final value denoted $x'$, we have | ||

- | \[ | + | \begin{equation*} |

r = \{(\{("x",x),("y",y)\},\{("x",x'),("y",y')\}) \mid x'=2y \land y' = y \} | r = \{(\{("x",x),("y",y)\},\{("x",x'),("y",y')\}) \mid x'=2y \land y' = y \} | ||

- | \] | + | \end{equation*} |

I will call the relation //r// the //relational semantics// of this command and the formula $x'=2y \land y'=y$ the //formula semantics// of this command. | I will call the relation //r// the //relational semantics// of this command and the formula $x'=2y \land y'=y$ the //formula semantics// of this command. | ||

When we have multiple variables, we can give semantics to assignment statements using [[sets and relations#function_update|function update notation]]. Regardless of the number of variables in $V$, the relational semantics of //x=y+y;// is | When we have multiple variables, we can give semantics to assignment statements using [[sets and relations#function_update|function update notation]]. Regardless of the number of variables in $V$, the relational semantics of //x=y+y;// is | ||

- | \[ | + | \begin{equation*} |

r = \{(s,s["x" \mapsto 2 s("y")]) \mid s \in S \} | r = \{(s,s["x" \mapsto 2 s("y")]) \mid s \in S \} | ||

- | \] | + | \end{equation*} |

===== Semantic Functions ===== | ===== Semantic Functions ===== | ||

Let $C$ denote the set of all commands (programs). Our goal is to define semantic function for commands, denoted $r_c$ (**r**elation of the **c**ommand), which maps each command $c_1$ into its relational semantics $r_c(c_1) \subseteq S \times S$. Formally, | Let $C$ denote the set of all commands (programs). Our goal is to define semantic function for commands, denoted $r_c$ (**r**elation of the **c**ommand), which maps each command $c_1$ into its relational semantics $r_c(c_1) \subseteq S \times S$. Formally, | ||

- | \[ | + | \begin{equation*} |

r_c : C \to 2^{S \times S} | r_c : C \to 2^{S \times S} | ||

- | \] | + | \end{equation*} |

To define meaning of statements such as //x=y+y;// we need a way to evaluate a term such as //y+y// in a given state. We introduce function $f_T$ (**f**unction of the **t**erm), which maps a term into a function from states to values: | To define meaning of statements such as //x=y+y;// we need a way to evaluate a term such as //y+y// in a given state. We introduce function $f_T$ (**f**unction of the **t**erm), which maps a term into a function from states to values: | ||

- | \[ | + | \begin{equation*} |

f_T : T \to (S \to R) | f_T : T \to (S \to R) | ||

- | \] | + | \end{equation*} |

Line 81: | Line 81: | ||

Given some definition of $f_T$, the meaning of the assignment statement is simply | Given some definition of $f_T$, the meaning of the assignment statement is simply | ||

- | \[ | + | \begin{equation*} |

r_c(x=e) = \{ (s,s["x" \mapsto f_T(e)(s)]) \mid s \in S \} | r_c(x=e) = \{ (s,s["x" \mapsto f_T(e)(s)]) \mid s \in S \} | ||

- | \] | + | \end{equation*} |

Line 99: | Line 99: | ||

Based on that context-free grammar, we can define recursively the terms semantic : | Based on that context-free grammar, we can define recursively the terms semantic : | ||

- | \[ | + | \begin{equation*} |

\begin{array}{lcl} | \begin{array}{lcl} | ||

f_T(k)(s) & = & k \\ | f_T(k)(s) & = & k \\ | ||

Line 115: | Line 115: | ||

f_T(f_1 | f_2)(s) & = & f_T(f_1)(s) \lor f_T(f_2)(s) | f_T(f_1 | f_2)(s) & = & f_T(f_1)(s) \lor f_T(f_2)(s) | ||

\end{array} | \end{array} | ||

- | \] | + | \end{equation*} |

Line 121: | Line 121: | ||

To execute a statement sequence, we execute the first statement and from the resulting state execute the second statement. We therefore define statement sequential composition as relation composition of statement meanings: | To execute a statement sequence, we execute the first statement and from the resulting state execute the second statement. We therefore define statement sequential composition as relation composition of statement meanings: | ||

- | \[ | + | \begin{equation*} |

r_c(c_1\ ;\ c_2) = r_c(c_1) \circ r_c(c_2) | r_c(c_1\ ;\ c_2) = r_c(c_1) \circ r_c(c_2) | ||

- | \] | + | \end{equation*} |

Line 138: | Line 138: | ||

To answer that question, we just have to derive these two expressions : | To answer that question, we just have to derive these two expressions : | ||

- | \[ | + | \begin{equation*} |

\begin{array}{lll} | \begin{array}{lll} | ||

& & r_c ( x = e_1 ; y = e_2 ) \\ | & & r_c ( x = e_1 ; y = e_2 ) \\ | ||

Line 145: | Line 145: | ||

& = & \{ ( s , ( s["x" \mapsto f_T(e_1)(s)] )["y" \mapsto f_T(e_2)( s["x" \mapsto f_T(e_1)(s) ] ) ] ) )~|~s \in S \} | & = & \{ ( s , ( s["x" \mapsto f_T(e_1)(s)] )["y" \mapsto f_T(e_2)( s["x" \mapsto f_T(e_1)(s) ] ) ] ) )~|~s \in S \} | ||

\end{array} | \end{array} | ||

- | \] | + | \end{equation*} |

Symetrically, we have: | Symetrically, we have: | ||

- | \[ | + | \begin{equation*} |

\begin{array}{lll} | \begin{array}{lll} | ||

& & r_c ( y = e_2 ; x = e_1 ) \\ | & & r_c ( y = e_2 ; x = e_1 ) \\ | ||

& = & \{ ( s , ( s["y" \mapsto f_T(e_2)(s)] )["x" \mapsto f_T(e_1)( s["y" \mapsto f_T(e_2)(s) ] ) ] ) )~|~s \in S \} | & = & \{ ( s , ( s["y" \mapsto f_T(e_2)(s)] )["x" \mapsto f_T(e_1)( s["y" \mapsto f_T(e_2)(s) ] ) ] ) )~|~s \in S \} | ||

\end{array} | \end{array} | ||

- | \] | + | \end{equation*} |

Thus, if y is free in $e_1$ and x is free in $e_2$, these two fragments will have the same meaning. | Thus, if y is free in $e_1$ and x is free in $e_2$, these two fragments will have the same meaning. | ||

Line 161: | Line 161: | ||

Assume statement is a useful declarative statement, which we will use to define the meaning of several remaining commands. The meaning of //assume// is simply is the diagonal relation, which produces no resulting states if the given expression is false, and does nothing if the expression is true: | Assume statement is a useful declarative statement, which we will use to define the meaning of several remaining commands. The meaning of //assume// is simply is the diagonal relation, which produces no resulting states if the given expression is false, and does nothing if the expression is true: | ||

- | \[ | + | \begin{equation*} |

r_c(\mbox{assume}(e)) = \{ (s,s) \mid f_T(e)(s) \} = \Delta_P | r_c(\mbox{assume}(e)) = \{ (s,s) \mid f_T(e)(s) \} = \Delta_P | ||

- | \] | + | \end{equation*} |

where $P = \{ s \mid f_T(e)(s) \}$. | where $P = \{ s \mid f_T(e)(s) \}$. | ||

Line 169: | Line 169: | ||

Non-deterministic choice is another useful declarative statement, which non-deterministically chooses to execute one of the two statements. We use it to express other statements, as well as to model branching with conditions that we cannot express in the language. Its meaning is simply union of relations: | Non-deterministic choice is another useful declarative statement, which non-deterministically chooses to execute one of the two statements. We use it to express other statements, as well as to model branching with conditions that we cannot express in the language. Its meaning is simply union of relations: | ||

- | \[ | + | \begin{equation*} |

r_c(c_1\ \mbox{[]}\ c_2) = r_c(c_1) \cup r_c(c_2) | r_c(c_1\ \mbox{[]}\ c_2) = r_c(c_1) \cup r_c(c_2) | ||

- | \] | + | \end{equation*} |

===== Representing if-then-else Using Non-Deterministic Choice and Assume ===== | ===== Representing if-then-else Using Non-Deterministic Choice and Assume ===== | ||

Line 184: | Line 184: | ||

We can also express this semantics directly as: | We can also express this semantics directly as: | ||

- | \[ | + | \begin{equation*} |

r_c(\mbox{if}(F)\mbox{ then } c_1 \mbox{ else } c_2) = \{ (s,s') \mid (f_T(F)(s) \land (s,s') \in r_c(c_1)) \lor (\lnot f_T(F)(s) \land (s,s') \in r_c(c_2) \} | r_c(\mbox{if}(F)\mbox{ then } c_1 \mbox{ else } c_2) = \{ (s,s') \mid (f_T(F)(s) \land (s,s') \in r_c(c_1)) \lor (\lnot f_T(F)(s) \land (s,s') \in r_c(c_2) \} | ||

- | \] | + | \end{equation*} |

Line 192: | Line 192: | ||

Just as we use non-deterministic choice (union) to represent conditional statment, we use non-deterministic loop statement (transitive closure) to represent while loops. A statement //loop( c )// executes statement //c// any number of times, possibly zero. Its meaning is transitive closure of the meaning of //c//. | Just as we use non-deterministic choice (union) to represent conditional statment, we use non-deterministic loop statement (transitive closure) to represent while loops. A statement //loop( c )// executes statement //c// any number of times, possibly zero. Its meaning is transitive closure of the meaning of //c//. | ||

- | \[ | + | \begin{equation*} |

r_c(\mbox{l{}o{}o{}p}(c_1)) = (r_c(c_1))^* | r_c(\mbox{l{}o{}o{}p}(c_1)) = (r_c(c_1))^* | ||

- | \] | + | \end{equation*} |

Line 236: | Line 236: | ||

Havoc statement is another useful declarative statement. It changes a given variable entirely arbitrarily: there will be one possible state for each possible value of integer variable. | Havoc statement is another useful declarative statement. It changes a given variable entirely arbitrarily: there will be one possible state for each possible value of integer variable. | ||

- | \[ | + | \begin{equation*} |

r_c(\mbox{havoc}(x)) = \{ (s,s') \mid \forall v \in V. v \neq "x" \rightarrow s(v)=s'(v) \} | r_c(\mbox{havoc}(x)) = \{ (s,s') \mid \forall v \in V. v \neq "x" \rightarrow s(v)=s'(v) \} | ||

- | \] | + | \end{equation*} |

==== Expressing Assignment with Havoc+Assume ==== | ==== Expressing Assignment with Havoc+Assume ==== | ||

We can prove that the following equality holds under certain conditions: | We can prove that the following equality holds under certain conditions: | ||

- | \[ | + | \begin{equation*} |

r_c(\mbox{havoc}(x);\mbox{assume}(x=e)) = r_c(x=e) | r_c(\mbox{havoc}(x);\mbox{assume}(x=e)) = r_c(x=e) | ||

- | \] | + | \end{equation*} |

In other words, assigning a variable is the same as changing it arbitrarily and then assuming that it has the right value. Under what condition does this equality hold? | In other words, assigning a variable is the same as changing it arbitrarily and then assuming that it has the right value. Under what condition does this equality hold? | ||

+ | |||

===== Summary of Correspondence between Programs and Relations ===== | ===== Summary of Correspondence between Programs and Relations ===== | ||

- | # program construct # relational meaning # | + | ^ program construct ^ relational meaning ^ |

| sequential composition | relation composition | | | sequential composition | relation composition | | ||

| branching | union | | | branching | union | | ||

Line 301: | Line 302: | ||

i = i - 1 | i = i - 1 | ||

as the relation $b$ whose formula is | as the relation $b$ whose formula is | ||

- | \[ | + | \begin{equation*} |

i > 0 \land r' = r + x \land i' = i - 1 | i > 0 \land r' = r + x \land i' = i - 1 | ||

- | \] | + | \end{equation*} |

We then wish to compute the transitive closure $b^* = \bigcup_{n \ge 0} b^n$. | We then wish to compute the transitive closure $b^* = \bigcup_{n \ge 0} b^n$. | ||

We claim that for every $n \ge 0$ relation $b^n$ is given by formula | We claim that for every $n \ge 0$ relation $b^n$ is given by formula | ||

- | \[ | + | \begin{equation*} |

i \ge n \land r' = r + n x \land i' = i - n | i \ge n \land r' = r + n x \land i' = i - n | ||

- | \] | + | \end{equation*} |

We can prove this claim by induction. The union of these relations is then given by | We can prove this claim by induction. The union of these relations is then given by | ||

- | \[ | + | \begin{equation*} |

\exists n \ge 0. i \ge n \land r' = r + n x \land i' = i - n | \exists n \ge 0. i \ge n \land r' = r + n x \land i' = i - n | ||

- | \] | + | \end{equation*} |

From there we can derive the meaning of | From there we can derive the meaning of | ||

<code> | <code> | ||

Line 325: | Line 326: | ||

</code> | </code> | ||

as | as | ||

- | \[ | + | \begin{equation*} |

\exists n \ge 0. y \ge n \land r' = n x \land i' = y - n | \exists n \ge 0. y \ge n \land r' = n x \land i' = y - n | ||

- | \] | + | \end{equation*} |

which when composed with //assume//($\neg (i > 0)$) = //assume//($i \leq 0$) gives | which when composed with //assume//($\neg (i > 0)$) = //assume//($i \leq 0$) gives | ||

- | \[ | + | \begin{equation*} |

\exists n \ge 0. y \ge n \land r' = n x \land i' = y - n \land i' \leq 0 | \exists n \ge 0. y \ge n \land r' = n x \land i' = y - n \land i' \leq 0 | ||

- | \] | + | \end{equation*} |

which is equivalent to | which is equivalent to | ||

- | \[ | + | \begin{equation*} |

y \ge 0 \land i' = 0 \land r' = y x | y \ge 0 \land i' = 0 \land r' = y x | ||

- | \] | + | \end{equation*} |

This is the semantics of the above code. | This is the semantics of the above code. | ||

Line 347: | Line 348: | ||

If $r$ is relation representing program and $s$ relation representing specification, we say that program meets specification iff | If $r$ is relation representing program and $s$ relation representing specification, we say that program meets specification iff | ||

- | \[ | + | \begin{equation*} |

r \subseteq s | r \subseteq s | ||

- | \] | + | \end{equation*} |

Example: | Example: | ||

Line 368: | Line 369: | ||

The correctness condition: | The correctness condition: | ||

- | \[ | + | \begin{equation*} |

\{ (v,v').\ v' = v + 1 \} \subseteq \{ (v,v').\ v > 0 \rightarrow v' > 0 \} | \{ (v,v').\ v' = v + 1 \} \subseteq \{ (v,v').\ v > 0 \rightarrow v' > 0 \} | ||

- | \] | + | \end{equation*} |

reduces to: | reduces to: | ||

- | \[ | + | \begin{equation*} |

\forall v. \forall v'.\ v' = v + 1 \rightarrow ( v > 0 \rightarrow v' > 0) | \forall v. \forall v'.\ v' = v + 1 \rightarrow ( v > 0 \rightarrow v' > 0) | ||

- | \] | + | \end{equation*} |

===== Further reading ===== | ===== Further reading ===== |