Skip to main content

Section D.7 Exercise Sheet 7

Recap C0 Statement Execution

1. Modulo Calculation.
  1. Execute the following program according to C0 semantics on the state

    \begin{equation*} \rho := \{a \mapsto \adra ,b \mapsto \adrb\}, \mu := \{\adra \mapsto 42, \adrb \mapsto 17\} \end{equation*}

    {
        while (a >= b)
            a = a - b;
        if (a == 8)
            abort();
        else
            b = 0;
    }
    

  2. Which kind of program stoppage occurs? How does it look when we instead choose \(\mu := \{\adra \mapsto 40, \adrb \mapsto 17\}\text{?}\) How does the program stop when we choose \(\mu := \{\adra \mapsto 42, \adrb \mapsto 0\}\text{?}\)

    Remark: A short explanation suffices.

202207281550

202205271400
Solution.
  1. To improve readability, we use the shorthand S for the if statement and W for the while statement.

    \(\langle \texttt{\{while(a>=b) a=a-b; S\}} \mid\)
    \(\rho, \{\adra \mapsto 42, \adrb \mapsto 17\} \rangle\)
    \(\rightarrow\) \(\langle \texttt{\{if(a>=b)\{a=a-b; W\} else \{\} S\}} \mid\)
    \(\rho, \{\adra \mapsto 42, \adrb \mapsto 17\}\rangle\)
    [While][Subst]
    \(\rightarrow\) \(\langle \texttt{\{\{a=a-b; W\} S\}} \mid\)
    \(\rho, \{\adra \mapsto 42, \adrb \mapsto 17\}\rangle\)
    [IfTrue][Subst]
    \(\rightarrow\) \(\langle \texttt{\{\{while(a>=b) a=a-b;\} S\}} \mid\)
    \(\rho, \{\adra \mapsto 25, \adrb \mapsto 17\}\rangle\)
    [Assign][Exec][Subst]
    \(\rightarrow\) \(\langle \texttt{\{\{if(a>=b)\{a=a-b; W\} else \{\}\} S\}} \mid\)
    \(\rho, \{\adra \mapsto 25, \adrb \mapsto 17\}\rangle\)
    [While][Subst][Subst]
    \(\rightarrow\) \(\langle \texttt{\{\{\{a=a-b; W\}\} S\}} \mid\)
    \(\rho, \{\adra \mapsto 25, \adrb \mapsto 17\}\rangle\)
    [IfTrue][Subst][Subst]
    \(\rightarrow\) \(\langle \texttt{\{\{\{while(a>=b) a=a-b;\}\} S\}} \mid\)
    \(\rho, \{\adra \mapsto 8, \adrb \mapsto 17\}\rangle\)
    [Assign][Exec][Subst][Subst]
    \(\rightarrow\) \(\langle \texttt{\{\{\{if(a>=b)\{a=a-b; W\} else \{\}\}\} S\}} \mid\)
    \(\rho, \{\adra \mapsto 8, \adrb \mapsto 17\}\rangle\)
    [While][Subst][Subst][Subst]
    \(\rightarrow\) \(\langle \texttt{\{\{\{\{\}\}\} S\}} \mid \rho, \{\adra \mapsto 8, \adrb \mapsto 17\}\rangle\) [IfFalse][Subst][Subst][Subst]
    \(\rightarrow\) \(\langle \texttt{\{\{\{\}\} S\}} \mid \rho, \{\adra \mapsto 8, \adrb \mapsto 17\}\rangle\) [Empty][Exec][Subst][Subst]
    \(\rightarrow\) \(\langle \texttt{\{\{\} S\}} \mid \rho, \{\adra \mapsto 8, \adrb \mapsto 17\}\rangle\) [Empty][Exec][Subst]
    \(\rightarrow\) \(\langle \texttt{\{if(a==8) abort(); else b=0;\}} \mid\)
    \(\rho, \{\adra \mapsto 8, \adrb \mapsto 17\}\rangle\)
    [Empty][Exec]
    \(\rightarrow\) \(\langle \texttt{\{abort();\}} \mid \rho, \{\adra \mapsto 8, \adrb \mapsto 17\}\rangle\) [IfTrue][Subst]
    \(\rightarrow\) \(\Lightning\) [Abort][Crash]
  2. The program aborts. For \(\mu := \{\adra \mapsto 40, \adrb \mapsto 17\}\) the program terminates in state \(\{ \adra \mapsto 6, \adrb \mapsto 0 \}\text{.}\) Except for the value of \(\adra\) the semantics is identical to part a). For \(\mu := \{\adra \mapsto 42, \adrb \mapsto 0\}\) the program diverges (does not stop) since the condition of the while loop is persistently true.

C0p

2. Syntax vs. Semantics.

There are syntactically correct C0 programs which get stuck during execution. Make yourself clear what the difference between syntax and semantics is. To this end, consider the following program. Is it syntactically or semantically correct? Can you find a different program which is syntactically, but not semantically correct? Can you find one that is syntactically incorrect but semantically correct?

{
    int x;
    x = 1337;
    x = x / 0;
}

202207281550

202205271400
Solution.

The syntax states how a valid C0 expression is built. The semantics describes how the expressions are evaluated. The above program is syntactically correct, but gets stuck because x / 0 is undefined. There are no programs which are semantically correct but syntactically incorrect because the semantics is only defined for a syntactically correct program. Another semantically incorrect program is:

{
    int x;
    x = 1337;
    x = y;
}

3. C0p - Basics.

Consider the state \(\sigma = (\rho,\mu)\) with

\begin{equation*} \rho := \{\texttt{x} \mapsto \adra, \texttt{y} \mapsto \adrb, \texttt{z} \mapsto \adrc\}, \mu := \{ \adra \mapsto \adrb, \adrb \mapsto 3, \adrc \mapsto \adra\}. \end{equation*}
  1. Build an expression which evaluates to \(1\) under \(\sigma\) according to C0p semantics. Use at least one * and & operator.

  2. Calculate the R-evaluation of your expression using the C0p rules.

202207281550

202205271400
Solution.
  1. *z == &y

  2. The expression evaluates to \(1\text{:}\)

    \begin{equation*} \denotR{\texttt{*z == \&y}} \sigma = \denotR{\texttt{*z}} \sigma \ \texttt{==} \ \denotR{\texttt{\&y}} \sigma = \adrb \ \texttt{==}\ \adrb = 1 \end{equation*}
    \begin{align*} \denotR{\texttt{*z}}\sigma \amp= \mu \denotL{\texttt{*z}} \sigma\\ \amp= \mu \denotR{\texttt{z}} \sigma \\ \amp= \mu ( \mu \denotL{\texttt{z}} \sigma) \\ \amp= \mu ( \mu (\rho(\texttt{z}) )) \\ \amp= \mu ( \mu (\adrc)) \\ \amp= \mu (\adra) \\ \amp= \adrb \end{align*}
    \begin{equation*} \denotR{\texttt{\&y}} \sigma = \denotL{\texttt{y}} \sigma = \rho(\texttt{y}) = \adrb \end{equation*}

4. C0p - More Pointers.
  1. Consider the state \(\sigma = (\rho; \mu)\) where

    \begin{align*} \rho \amp:= \{ \texttt{x} \mapsto \adra, \texttt{y} \mapsto \adrd, \texttt{t} \mapsto \adrb, \texttt{z} \mapsto \adre \}\\ \mu \amp:= \{ \adra \mapsto \adrc, \adrb \mapsto 10, \adrd \mapsto \square, \adrc \mapsto 4, \square \mapsto 2, \adre \mapsto \indetval \} \end{align*}

    Write a C0p program which assigns the value \(42\) to z. Use only the variables used above, in particular do not use constants.

  2. Check your program by applying the operational semantics of C0p.

  3. In the following expressions, errors could occur. Correct them if present and state a configuration such that the program has a semantics. Assume that all variables have been declared.

    1. {
          x = 0;
          *p = &x+2;
      }
      
    2. {
          x = 0;
          *p = &x;
          **pP = &*p;
      }
      
202207281550

202205271400
Solution.
  1. z = *x * t + *y;

  2. Execution:

    \(\langle \texttt{z = *x * t + *y}; {}\mid{} \rho; \{ \adra \mapsto \adrc, \adrb \mapsto 10, \adrd \mapsto \square, \adrc \mapsto 4, \square \mapsto 2, \adre \mapsto\indetval \} \rangle\)
    \(\rightarrow\) \(\rho; \{ \adra \mapsto \adrc, \adrb \mapsto 10, \adrd \mapsto \square, \adrc \mapsto 4, \square \mapsto 2, \adre \mapsto 42 \}\) [Assign]
    \begin{align*} \denotR{\texttt{*x * t + *y}} \sigma \amp= \denotR{\texttt{*x * t}} \sigma + \denotR{\texttt{*y}} \sigma\\ \amp= \denotR{\texttt{*x}} \sigma * \denotR{\texttt{t}} \sigma + \denotR{\texttt{*y}} \sigma\\ \amp= \mu(\denotL{\texttt{*x}} \sigma) * \denotR{\texttt{t}} \sigma + \mu(\denotL{\texttt{*y}} \sigma)\\ \amp= \mu(\denotR{\texttt{x}} \sigma) * \denotR{\texttt{t}} \sigma + \mu(\denotR{\texttt{y}} \sigma)\\ \amp= \mu(\mu(\denotL{\texttt{x}} \sigma)) * \mu(\denotL{\texttt{t}} \sigma) + \mu(\mu(\denotL{\texttt{y}} \sigma))\\ \amp= \mu(\mu(\rho(\texttt{x}))) * \mu(\rho(\texttt{t})) + \mu(\mu(\rho(\texttt{y})))\\ \amp= \mu(\mu(\adra)) * \mu(\adrb) + \mu(\mu(\adrd))\\ \amp= \mu(\adrc) * 10 + \mu(\square)\\ \amp= 4 * 10 + 2\\ \amp= 42 \end{align*}
    1. We cannot use &x + 2 since we have no pointer arithmetic in C0p. A possible correction:

      x = 0;
      *p = &x;
      

      Configuration: \(\sigma := \{ \texttt{x} \mapsto \adrd, \texttt{p} \mapsto \adrb \}; \{ \adrd \mapsto \indetval, \adrb \mapsto \adrc, \adrc \mapsto \indetval \}\)

    2. There are no errors. Configuration: \(\sigma := \{ \texttt{x} \mapsto \adrd, \texttt{p} \mapsto \adrb, \texttt{pP} \mapsto \square \}; \{ \adrd \mapsto \indetval, \adrb \mapsto \adrc, \adrc \mapsto \indetval, \square \mapsto \adrb \}\)

5. Pointers and Semantics.

Execute the following C0p program on the state \(\sigma = (\rho; \mu) = \{\texttt{x}\mapsto \adra, \texttt{y} \mapsto \adrb\}; \{\adra \mapsto \indetval, \adrb \mapsto \indetval\}\)

{
    x = 3;
    y = &x;
    *y = *y + 1;
}

Explicitly state the evaluation of \(\denotR{\texttt{\&x}}\) and \(\denotR{\texttt{*y + 1}}\text{.}\)

202207281550

202205271400
Solution.
\(\langle \texttt{\{x = 3; y = \&x; *y = *y + 1;\}} \mid \rho; \{\adra \mapsto \indetval, \adrb \mapsto \indetval \}\rangle\)
\(\rightarrow\) \(\langle \texttt{\{y = \&x; *y = *y + 1;\}} \mid \rho; \{\adra \mapsto 3, \adrb \mapsto \indetval \}\rangle\) [Assign][Exec]
\(\rightarrow\) \(\langle \texttt{\{*y = *y + 1;\}} \mid \rho; \{\adra \mapsto 3, \adrb \mapsto \adra \}\rangle\) [Assign][Exec]
\(\rightarrow\) \(\langle \texttt{\{\}} \mid \rho; \{\adra \mapsto 4, \adrb \mapsto \adra \}\rangle\) [Assign][Exec]
\(\rightarrow\) \(\rho; \{\adra \mapsto 4, \adrb \mapsto \adra \}\) [Empty]
\begin{equation*} \denotR{\texttt{\&x}} \sigma = \denotL{\texttt{x}} \sigma = \rho(\texttt{x}) = \adra \end{equation*}
\begin{align*} \denotR{\texttt{*y + 1}} \sigma \amp= \denotR{\texttt{*y}} \sigma + \denotR{1} \sigma\\ \amp= \mu(\denotL{\texttt{*y}} \sigma) + 1\\ \amp= \mu(\denotR{\texttt{y}} \sigma) + 1\\ \amp= \mu(\mu(\denotL{\texttt{y}} \sigma)) + 1\\ \amp= \mu(\mu(\rho(\texttt{y}))) + 1\\ \amp= \mu(\mu(\adrb)) + 1\\ \amp= \mu(\adra) + 1\\ \amp= 3 + 1\\ \amp= 4 \end{align*}
6. Double Pointers.

Execute the following C0p program on the state \(\sigma = (\rho; \mu)\) where

\begin{align*} \rho \amp:= \{ \texttt{x} \mapsto \adra, \texttt{y} \mapsto \adrb, \texttt{z} \mapsto \adrc, \texttt{w} \mapsto \adrd\}\\ \mu \amp:= \{\adra \mapsto \indetval, \adrb \mapsto \indetval, \adrc \mapsto \indetval, \adrd \mapsto \indetval\} \end{align*}

{
  x = 42;
  y = &x;
  z = &y;
  w = **z;
}

Observe especially how the containers are “linked”.

202207281550

202205271400
Solution.
\(\langle \texttt{\{x = 42; y = \& x; z = \& y; w = **z;\}} \mid\)
\(\rho; \{ \adra \mapsto \indetval, \adrb \mapsto \indetval, \adrc \mapsto \indetval, \adrd \mapsto \indetval \} \rangle\)
\(\rightarrow\) \(\langle \texttt{\{y = \&x; z = \&y; w = **z;\}} \mid \rho; \{ \adra \mapsto 42, \adrb \mapsto \indetval, \adrc \mapsto \indetval, \adrd \mapsto \indetval \} \rangle\) [Assign][Exec]
\(\rightarrow\) \(\langle \texttt{\{z = \&y; w = **z;\}} \mid \rho; \{ \adra \mapsto 42, \adrb \mapsto \adra, \adrc \mapsto \indetval, \adrd \mapsto \indetval \} \rangle\) [Assign][Exec]
\(\rightarrow\) \(\langle \texttt{\{w = **z;\}} \mid \rho; \{ \adra \mapsto 42, \adrb \mapsto \adra, \adrc \mapsto \adrb, \adrd \mapsto \indetval \} \rangle\) [Assign][Exec]
\(\rightarrow\) \(\langle \texttt{\{\}} \mid \rho; \{ \adra \mapsto 42, \adrb \mapsto \adra, \adrc \mapsto \adrb, \adrd \mapsto 42 \} \rangle\) [Assign][Exec]
\(\rightarrow\) \(\rho; \{ \adra \mapsto 42, \adrb \mapsto \adra, \adrc \mapsto \adrb, \adrd \mapsto 42 \}\) [Empty]
7. C0p - Reloaded.

Execute the following program according to the C0p semantics adrating in the state \(\sigma = (\rho; \mu)\) where

\begin{gather*} \rho := \{ \texttt{a}\mapsto \adra, \texttt{i} \mapsto \adre, \texttt{k} \mapsto \adrd, \texttt{n} \mapsto \adrc, \texttt{c} \mapsto \adrf \}\\ \mu := \{ \adrf \mapsto 1, \adra \mapsto \adrf, \adrd \mapsto 2, \adre \mapsto 0, \adrc \mapsto 2 \} \end{gather*}

while(i < n) {
    *a = *a * k;
    i = i + 1;
}

Which value resides in c after the program has finished?

Can you state a general formula for the content of c (for arbitrary \(n, k \in \mathbb{N}\))?

202207281550

202205271400
Solution.

In the following, we shorten *a = *a * k; i = i + 1; by S and while(i < n) {*a = *a * k; i = i + 1;} by W.

\(\langle \texttt{while(i < n) S} {}\mid{} \rho; \{ \adrf \mapsto 1, \adra \mapsto \adrf, \adrd \mapsto 2, \adre \mapsto 0, \adrc \mapsto 2 \} \rangle\)
\(\to\) \(\langle \texttt{if(i < n) \{S while(i < n) S\} else \{\}} {}\mid{} \rho; \mu \rangle\) [While]
\(\to\) \(\langle \texttt{\{*a = *a * k; i = i+1; W\}} {}\mid{} \rho; \mu \rangle\) [IfTrue]
\(\to\) \(\langle \texttt{\{i = i+1; W\}} {}\mid{} \rho; \{ \adrf \mapsto 2, \adra \mapsto \adrf, \adrd \mapsto 2, \adre \mapsto 0, \adrc \mapsto 2 \} \rangle\) [Assign][Exec]
\(\to\) \(\langle \texttt{\{while(i < n) S\}} {}\mid{} \rho; \{ \adrf \mapsto 2, \adra \mapsto \adrf, \adrd \mapsto 2, \adre \mapsto 1, \adrc \mapsto 2 \} \rangle\) [Assign][Exec]
\(\to\) \(\langle \texttt{\{if(i < n) \{S while(i < n) S\} else \{\}\}} {}\mid{} \rho; \mu \rangle\) [While][Subst]
\(\to\) \(\langle \texttt{\{\{*a = *a * k; i = i+1; W\}\}} {}\mid{} \rho; \mu \rangle\) [IfTrue][Subst]
\(\to\) \(\langle \texttt{\{\{i = i+1; W\}\}} {}\mid{} \rho; \{ \adrf \mapsto 4, \adra \mapsto \adrf, \adrd \mapsto 2, \adre \mapsto 1, \adrc \mapsto 2 \} \rangle\) [Assign][Exec][Subst]
\(\to\) \(\langle \texttt{\{\{while(i < n) S\}\}} {}\mid{} \rho; \{ \adrf \mapsto 4, \adra \mapsto \adrf, \adrd \mapsto 2, \adre \mapsto 2, \adrc \mapsto 2 \} \rangle\) [Assign][Exec][Subst]
\(\to\) \(\langle \texttt{\{\{if(i < n) \{S while(i < n) S\} else \{\}\}\}} {}\mid{} \rho; \mu \rangle\) [While][Subst][Subst]
\(\to\) \(\langle \texttt{\{\{\{\}\}\}} {}\mid{} \rho; \mu \rangle\) [IfFalse][Subst][Subst]
\(\to\) \(\langle \texttt{\{\{\}\}} {}\mid{} \rho; \mu \rangle\) [Empty][Exec][Subst]
\(\to\) \(\langle \texttt{\{\}} {}\mid{} \rho; \mu \rangle\) [Empty][Exec]
\(\to\) \(\rho; \{ \adrf \mapsto 4, \adra \mapsto \adrf, \adrd \mapsto 2, \adre \mapsto 2, \adrc \mapsto 2 \}\) [Empty]

If n initially has the value \(m\) and k initially has the value \(j\text{,}\) then c will be n to the power of k.

C0pb

8. Transforming Blocks.
  1. Change the following program such that the braces of the inner block vanish, the amount of variable declarations stays the same, and the value of y at the end of the outer block is still the same.

    { 
        int y;
        int x;
        x = 42;
        {
            int x;
            x = 7;
        }
        y = x;
    }
    

  2. Describe an algorithm that removes nested blocks without changing the semantics of the program.

  3. Will the following program still behave the same after applying your algorithm?

    {
        int x;
        int y;
        int i;
        x = 42;
        i = 0;
        while (i < 2) {
            int x;
            if (i == 0){
                x = 0;
            }
            y = x;
            i = i+1;
        }
    }
    
    If not, is an optimizing C compiler allowed to apply this transformation anyway?

202207281550

202205271400
Solution.
  1. {
        int y;
        int x;
        int x1;
        x = 42;
        x1 = 7;
        y = x;
    }
    

    1. Starting in the innermost block: If a block declares a variable that is already declared outside of the block, rename the variable to an unused identifier and substitute all occurences accordingly.

    2. Now move every variable declaration to the parent block.

    3. Remove the block.

  2. This is not the case with our algorithm. The original program gets stuck in the second loop iteration, since x is undefined. After applying the algorithm, x1 is however bound to \(0\) and the program does not get stuck anymore.

    In C, a program that gets stuck has undefined behaviour, therefore it would be legitimate for a C compiler to apply this transformation, as the compiler may assume that undefined behaviour does not occur.

    {
        int x;
        int y;
        int i;
        int x1;
        x = 42;
        i = 0;
        while (i < 2) {
            if (i == 0) {
                x1 = 0;
            }
            y = x1;
            i = i+1;
        }
    }
    

9. Dangling Pointers.

A pointer is dangling if it refers to an address for which there is no container. Construct a C0pb program which contains a dangling pointer during execution. Verify this by executing the program according to the C0 semantics.

202207281550

202205271400
Solution.

 {
    int x;
    int *p;
    {
        int y;
        p = &y;
    }
    x = *p;
}

The pointer p points to a container which does not exist anymore after execution of the block. The semantics gets stuck after at the statement x = *p;:

\(\langle \texttt{\{ int x; int *p; \{ int y; p = \&y; \} x = *p; \}} \mid \{ \};\{ \} \rangle\)
\(\rightarrow\) \(\langle \texttt{\{\{ int y; p = \&y; \} x = *p;} {}\cleave{} \} \mid \{\},\{ \texttt{x} \mapsto \adra, \texttt{p} \mapsto \adrb \}; \{ \adra \mapsto \indetval, \adrb \mapsto \indetval \} \rangle\) [Scope]
\(\rightarrow\) \(\langle \{\{ \texttt{p = \&y;} {}\cleave{} \} \texttt{x = *p;} {}\cleave{} \} \mid \{\},\{ \texttt{x} \mapsto \adra, \texttt{p} \mapsto \adrb\},\{\texttt{y} \mapsto \adrc \}; \{ \adra \mapsto \indetval, \adrb \mapsto \indetval, \adrc \mapsto \indetval \} \rangle\) [Scope][Subst]
\(\rightarrow\) \(\langle \{\{{}\cleave{}\} \texttt{x = *p;} {}\cleave{}\} \mid \{\},\{ \texttt{x} \mapsto \adra, \texttt{p} \mapsto \adrb\},\{\texttt{y} \mapsto \adrc \}; \{ \adra \mapsto \indetval, \adrb \mapsto \adrc, \adrc \mapsto \indetval \} \rangle\) [Assign][Exec][Subst]
\(\rightarrow\) \(\langle \{\texttt{x = *p;} {}\cleave{}\} \mid \{\},\{ \texttt{x} \mapsto \adra, \texttt{p} \mapsto \adrb \}; \{ \adra \mapsto \indetval, \adrb \mapsto \adrc \} \rangle\) [Leave][Exec]
\begin{align*} \denotR{\texttt{*p}} \sigma \amp = \mu(\denotL{\texttt{*p}} \sigma)\\ \amp = \mu(\denotR{\texttt{p}} \sigma)\\ \amp = \mu(\mu(\denotL{\texttt{p}} \sigma))\\ \amp = \mu(\mu(\rho(\texttt{p})))\\ \amp = \mu(\mu(\adrb))\\ \amp = \mu(\adrc) \quad \Lightning \end{align*}

The container \(\adrc\) does not exist anymore, so the rule “Assign” is not applicable.

10. C0b Execution.

Execute the following C0b statements, if possible! Start with the empty state. If the program is not syntactically valid, state why!

  1. {
      int x;
      x = 42;
      {
        int x;
        x = 24;
        {
          int z;
          z = x * 7;
        }
      }
      x = x + 11;
    }
    
  2. {
      int x;
      int y;
      x = 5;
      y = 7;
      {
        int z;
        z = 5;
        y = 21;
      }
      x = x + y;
    }
    
  3. {
      {
        int x;
        x = 13;
        int y;
        y = x * 5;
      }
      int z;
      y = z + x;
    }
    
202207281550

202205271400
Solution.
  1. Execution:

    Figure D.7.1.
  2. Execution:

    Figure D.7.2.
  3. Our syntax for C0b only allows declarations at the beginning of a block. Even when all declaration are moved to the beginning the program, it is semantically invalid. The reading of x and the writing to y outside of the corresponding visibility scopes (in line 9) are invalid. There is no derivation, the program therefore gets stuck.

11. More C0b Execution.

Derive the following C0b statements, if possible! Start with the empty state.

{
  int a;
  int b;
  b = 15;
  a = b + 2;
  {
    int b;
    b = a;
    a = b - 1;
  }
  b = b + 3;
  b = b + a;
}

202207281550

202205271400
Solution.

Execution:

Figure D.7.3.

Testing

12. Writing Specifications for Programs.

Write a formal specification for the programs below.

  1. if (n < m) {
        k = n;
    } else {
        k = m;
    }
    

  2. {
        x = n/m;
        if (x <= 0){
            x = -n/m
        }
    }
    

  3. if (x > 1) {
        y = 4 * x + 2;
        z = y / 2;
        x = y + z + 1;
        x--;
        x = x / 3;
    } else {
        x++;
    }
    

202207281550

202205271400
Solution.
  1. The program stores \(\min\{m, n\}\) in \(k\text{:}\)

    \begin{equation*} \{(\sigma,\sigma') \mid \sigma'k \leq \sigma m \land \sigma'k \leq \sigma n \land (\sigma' k = \sigma n \lor \sigma' k = \sigma m)\} \end{equation*}
  2. The program calculates the absolute value of the fraction \(\frac{n}{m}\text{:}\)

    \begin{align*} \{(\sigma,\sigma') &\mid \sigma m \neq 0 \Rightarrow (((\sigma m < 0 \land \sigma n \geq 0) \lor (\sigma m \geq 0 \land n < 0)) \land \sigma'x = -\frac{\sigma n}{\sigma m}) {}\lor{}\\ &(((\sigma m \geq 0 \land \sigma n \geq 0) \lor (\sigma m < 0 \land \sigma n < 0)) \land \sigma' x = \frac{\sigma n}{\sigma m})\} \end{align*}

    Alternatively:

    \begin{equation*} \{(\sigma,\sigma') \mid \sigma m \neq 0 \Rightarrow \sigma' x=|\frac{\sigma n}{\sigma m}| \} \end{equation*}
  3. \begin{align*} \{(\sigma,\sigma') &\mid (\sigma x \leq 1 \land \sigma'x = \sigma x + 1) {}\lor{}\\ &(\sigma x > 1 \land \sigma'x = \sigma'z = 2 * \sigma x + 1 \land \sigma'y = 4 * \sigma x + 2)\} \end{align*}
13. Constructing Specifications.

Describe the C0 programs depicted below formally by stating the corresponding program specifications. Try to formulate the specifications as shortly as possible.

  1. if (n >= 0) {
        n = n;
    } else {
        n = (-7) * 3 + n * (-1) + 21;
    }
    

  2. while (b > 0) {
        x += a;
        b--;
    }
    

  3. if (a < b) {
        if (a < 10) {
            max = a;
        } else {
            max = 10;
        }
    } else {
        if (b < 10) {
            max = b;
        } else {
            max = 10;
        }
    }
    

202207281550

202205271400
Solution.
  1. \begin{equation*} S_{\operatorname{abs}} = \left\{ (\sigma, \sigma') \mid \sigma n = |\sigma'n| \right\} \end{equation*}
  2. \begin{align*} S_{\operatorname{mul}} = \{ (\sigma, \sigma') &\mid (\sigma b > 0 \Rightarrow \sigma' x = \sigma x + \sigma a * \sigma b \land \sigma' b = 0)\\ &{}\land{} (\sigma b \leq 0 \Rightarrow \sigma' x = \sigma x \land \sigma b = \sigma' b) \} \end{align*}
  3. \begin{align*} S_{\min} = \{ (\sigma, \sigma') &\mid ( (\sigma a \geq 10 \wedge \sigma b \geq 10) \Rightarrow \sigma' max = 10)\\ &\land ( (\sigma a < 10 \vee \sigma b < 10) \Rightarrow \sigma' max = \min(\sigma a, \sigma b ) ) \} \end{align*}

    where \(\min(a, b)\) has the intuitive definition:

    \begin{equation*} \min(a,b) = \begin{cases} a & \mbox{if } a < b \\ b & \mbox{otherwise} \end{cases} \end{equation*}
14. Program to Specification.
  1. For the following specifications, construct a C0b program that implements it.

    1. \(\displaystyle S_1 = \{(\sigma, \sigma') \,|\, \sigma' x = \sigma x + \sigma y\}\)

    2. \(\displaystyle S_2 = \{(\sigma, \sigma') \,|\, \sigma' x = (\sigma x)^{100}\}\)

    3. \(\displaystyle S_3 = \{(\sigma, \sigma') \,|\, \sigma' x > \sigma' y\}\)

    4. \(S_4 = \{(\sigma, \sigma') \,|\, \sigma' x = (\sigma x)!\}\) with \(n! = 1 \cdot 2 \cdot ... \cdot n = \prod_{k=1}^n k\text{.}\)

    5. \(S_5 = \{(\sigma, \sigma') \,|\, \sigma'g = \text{gcd}(\sigma x, \sigma y)\}\) where \(gcd(x, y)\) is the greatest common divisor of \(x\) and \(y\text{.}\)

  2. Construct a program which implements the specification \((P,Q)\) for the following \(P\) and \(Q\text{:}\)

    1. \begin{equation*} P = x \neq 0 \quad Q = (d = \frac{y}{x}) \end{equation*}
    2. \begin{equation*} P = true \quad Q = (d = \frac{y}{x} \lor x = 0) \end{equation*}
    3. \begin{equation*} P = true \quad Q = (a = x + y) \end{equation*}
202207281550

202205271400
Solution.
    1. x = x + y;
      

    2. {
          int y;
          int x0; 
          x0 = x; 
          y = 100; 
          while (y != 1) {
              x = x * x0;
              y = y - 1;
          }
      }
      

    3. x = y + 1;
      

    4. {
          int y; 
          y = x - 1;
          while (y != 0) {
              x = x * y;
              y = y - 1;
          }
      }
      

    5. {
          while(y != 0) {
              int h; 
              h = x % y;
              x = y; 
              y = h;
          } 
          g = x;
      }
      

    1. d = y / x;
      

    2. if (x == 0) {}
      else 
          d = y / x;
      

    3. a = x + y;
      

15. Implementing a Specification.
  1. Write a C0 program which implements the following specification:

    \begin{align*} S = \{ (\sigma, \sigma') \mid & \sigma\,x > 1 \implies \sigma'\,y = \sigma\,b \, {}\land{}\\ & \sigma\,x < 0 \implies \sigma'\,y = \sigma\,a \, {}\land{}\\ & \sigma\,x \ge 0 \land \sigma\,x \le 1 \implies \sigma'\,y = \sigma\,x \cdot \sigma\,b + (1 - \sigma\,x) \cdot\sigma\,a \} \end{align*}
  2. Prove that your program is correct. To this end, make a case distinction for the input (\(\sigma\,x > 1\text{,}\) etc.) and then execute the program for every case using the operational semantics of C0.

202207281550

202205271400
Solution.
  1. if (x > 1)
        y = b;
    else if (x < 0)
        y = a;
    else
        y = x * b + (1 - x) * a;
    

  2. We consider the three possible cases independently. Let \((\sigma, \sigma') \in S\) be arbitrary but fixed.

    • Case \(\sigma\,x > 1\text{.}\) In order for \((\sigma,\sigma')\) to implement the specification, we must have \(\sigma'\, y = \sigma\, b\) after execution.

      1. \begin{equation*} \begin{prooftree} \AxiomC{$ \sigma\,x > 1$} \LeftLabel{[IfTrue]$\qquad\quad$} \UnaryInfC{$ \config{\texttt{if } (x > 1) \ y = b; \texttt{ else } ...} {\sigma} \steprel \config{ y = b; } {\sigma}$} \end{prooftree} \end{equation*}
      2. \begin{equation*} \begin{prooftree} \AxiomC{$ $} \LeftLabel{[Assign]$\qquad\quad$} \UnaryInfC{$ \config{ y = b; } {\sigma} \steprel \sigma[y \mapsto \sigma\, b]$} \end{prooftree} \end{equation*}

      From the last state \(\sigma' = \sigma[y \mapsto \sigma \,b]\text{,}\) it follows that \(\sigma'\, y = \sigma \,b\text{.}\)

    • Case \(\sigma\,x < 0\text{.}\) In order for \((\sigma,\sigma')\) to implement the specification, we must have \(\sigma'\, y = \sigma\, a\) after execution.

      1. \begin{equation*} \begin{prooftree} \AxiomC{$\sigma\,x < 0 $} \LeftLabel{[IfFalse]$\qquad\quad$} \UnaryInfC{$\config{\texttt{if } (x > 1) \ y = b; \texttt{ else } \texttt{if } (x < 0) \ y = a; \texttt{ else } ...} {\sigma} \steprel \config{ \texttt{if } (x < 0)\ y = a; \texttt{ else } ...} {\sigma} $} \end{prooftree} \end{equation*}
      2. \begin{equation*} \begin{prooftree} \AxiomC{$\sigma\,x < 0$} \LeftLabel{[IfTrue]$\qquad\quad$} \UnaryInfC{$\config{\texttt{if } (x < 0)\ y = a; \texttt{ else } ...} {\sigma} \steprel \config{ y = a; } {\sigma}$} \end{prooftree} \end{equation*}
      3. \begin{equation*} \begin{prooftree} \AxiomC{$ $} \LeftLabel{[Assign]$\qquad\quad$} \UnaryInfC{$\config{ y = a; } {\sigma} \steprel \sigma[y \mapsto \sigma\,a]$} \end{prooftree} \end{equation*}

      From the last state \(\sigma' = \sigma[y \mapsto \sigma\,a]\text{,}\) it follows that \(\sigma'\, y = \sigma \,a\text{.}\)

    • Case \(\sigma\,x\ge 0 \land \sigma\,x\le 1\text{.}\) In order for \((\sigma,\sigma')\) to implement the specification, we must have \(\sigma' y = \sigma\,x\cdot\sigma\,b + (1 - \sigma\,x)\cdot\sigma\,a\) after execution.

      1. \begin{equation*} \begin{prooftree} \AxiomC{$\sigma\,x\ge 0 \land \sigma\,x\le 1$} \LeftLabel{[IfFalse]$\qquad\quad$} \UnaryInfC{$\config{\texttt{if } (x > 1)\ y = b; \texttt{ else } \texttt{if } (x < 0)\ y = a; \texttt{ else } ...} {\sigma} \steprel \config{ \texttt{if } (x < 0)\ y = a; \texttt{ else } ...} {\sigma}$} \end{prooftree} \end{equation*}
      2. \begin{equation*} \begin{prooftree} \AxiomC{$\sigma\,x\ge 0 \land \sigma\,x\le 1$} \LeftLabel{[IfFalse]$\qquad\quad$} \UnaryInfC{$\config{\texttt{if } (x < 0)\ y = a; \texttt{ else } y = x * b + (1 - x) * a; } {\sigma} \steprel \config{ y = x * b + (1 - x) * a; } {\sigma}$} \end{prooftree} \end{equation*}
      3. \begin{equation*} \begin{prooftree} \AxiomC{$ $} \LeftLabel{[Assign]$\qquad\quad$} \UnaryInfC{$\config{ y = x * b + (1 - x) * a; } {\sigma} \steprel \sigma[y \mapsto \sigma\,x\cdot\sigma\,b + (1 - \sigma\,x) \cdot\sigma\,a]$} \end{prooftree} \end{equation*}

      From the last state \(\sigma' = \sigma[y \mapsto \sigma\,x\cdot\sigma\,b + (1 - \sigma\,x) \cdot\sigma\,a]\text{,}\) it follows that \(\sigma' y = \sigma\,x\cdot\sigma\,b + (1 - \sigma\,x)\cdot\sigma\,a\text{.}\)

16. Assertions.

Write assertions inside the gap marked by ... such that the function supersum always terminates.

int supersum(int a, int b, int c) {
    assert(c >= 0);

    ...

    int x = 0;
    for (int i = a; x < b; i = i + c) {
        x = x + i;
    }
    return x;
}

202207281550

202205271400
Solution.

int supersum(int a, int b, int c) {
    assert(c >= 0);

    assert(
        // the program terminates without entering the loop
        (b <= 0) ||

        // the loop stops after the first iteration 
        (a >= b) ||  

        // i will be positive eventually and therefore x will eventually be greater than b
        (c > 0)  ||

        // x will be increased by the positive value a in every iteration 
        (c == 0 && a > 0)
    );

    int x = 0;
    for (int i = a; x < b; i = i + c) {
        x = x + i;
    }
    return x;
}
Tip: To get detailed error messages, it makes sense to split a conjunctive assertion into multiple assertions. For example, it makes sense to write assert(x>=0); assert(y>=0); instead of assert(x>=0 && y>=0);.