Software Specification Exercises: Separation Logic

Software Specification, MEIC @ IST, 2019/20

jff

## Instructions - You can use the arrow keys, PgDown and PgUp to browse these exercises - You can use Escape to see an overview - You can use Ctrl+Click to zoom in

## 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

Draw/Determine the stack and heap corresponding to the following formulae:

$x=3 \wedge y=4 \,\ast\, emp$
$x \mapsto 4,5$
$y=3 \,\wedge\, x \mapsto 4,5$
$x \mapsto 4,4 \,\ast\, y \mapsto 4,4$

2. Assertions

Say if the following are valid or not:

$x \mapsto 3 \,\ast\, y \mapsto 7 \,\,\Rightarrow\,\, x \mapsto 3 \,\ast\, true$
$true \,\ast\, x \mapsto 3 \,\,\Leftrightarrow\,\, x \mapsto 3$

3. Annotations

Prove the following triple by annotating the program:

$$ \{emp\} \\ x := cons(1,2); \\ y := cons(3,4); \\ [y+1] := [x+1]; \\ dispose\ \ x; \\ \{y \mapsto 3,2\} $$

4. Invariants

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)} $$