## Introduction
The goal of this lab is to get more familiar with
separation logic assertions.
### 0. Before you continue
Make sure that you do all the exercises from previous
sessions (if you haven't done so already).
1. Assertions (Solutions)
Draw/Determine the stack and heap corresponding to the
following formulae:
- $x=3 \wedge y=4 \,\ast\, emp$
- Store: $x: 3, y: 4$
- Heap: empty
- $x \mapsto 4,5$
- Store: $x: 42$ (here and below, 42 is an arbitrary address)
- Heap: $42: 4, 43: 5$
- $y=3 \,\wedge\, x \mapsto 4,5$
- Store: $y: 3, x: 42$
- Heap: $42: 4, 43: 5$
- $x \mapsto 4,4 \,\ast\, y \mapsto 4,4$
- Store: $x: 42, y: 44$
- Heap: $42: 4, 43: 4, 44: 4, 45: 4$
2. Assertions (Solutions)
Say if the following are valid or not:
- $x \mapsto 3 \,\ast\, y \mapsto 7 \,\,\Rightarrow\,\, x \mapsto 3 \,\ast\, true$
True
- $true \,\ast\, x \mapsto 3 \,\,\Leftrightarrow\,\, x
\mapsto 3$
False
3. Annotations (Solutions)
Prove the following triple by annotating the program:
$$
\{emp\} \\
x := cons(1,2); \\
\{ x \mapsto 1,2 \} \\
y := cons(3,4); \\
\{ x \mapsto 1,2 \ \ast\ y \mapsto 3,4 \} \\
[y+1] := [x+1]; \\
\{ x \mapsto 1,2 \ \ast\ y \mapsto 3,2 \} \\
dispose\ \ x; \\
\{y \mapsto 3,2\}
$$
4. Invariants (Solution)
Propose a loop invariant for proving the following
partial correctness triple in separation logic:
$$
\ht{(N \geq 0 \,\wedge\, X=0) \wedge Y \mapsto 0}
{C}
{Y
\mapsto \sum_{i=1}^{N-1}{i}}
$$
where $C$ is:
$$
\whileloop{X \lt N}{(A := [Y]; X := X+1; [Y] := A+X)}
$$
Solution:
$$Y \mapsto \sum_{i=1}^{X-1}{i}
\,\,\wedge\,\,
X \leq N$$