# LARA

## Asserts and errors for nice wp definition

We used assert(F) to express conditions that should hold.

Can we give executation semantics to assert?

assert(F) = irrecoverable error if is false, terminates execution.

wp computes conditions sufficient for errors not to happen.

Postconditions are just asserts at the end of the program.

How to build a system with relations where at the same time

wp(assert(F),Q) = (F & Q)
wp(assume(F),Q) = (F --> Q)

Then

wp(assert(false); assume(false),Q) = false
wp(assume(false); assert(false),Q) = true

so cannot have any more, otherwise both

assert(false); assume(false)
assume(false); assert(false)

would denote empty relations.

## Error Variable and Good States

Introduce variable “error”. Good states are states where this variable has value zero. We write OK for the formula error=0.

We assume that the desired properties satisfy

## Desired Rules for Weakest Preconditions

For all such that , we would like the following to hold:

We assume above that is not the error variable.

Note: we wrote in the weakest precondition of assume, but usually is implicit and we do not write it. We do not need it in other cases because it follows that right hand side implies .

## Relational Semantics that Fulfills These Rules

Let OK denote s(error)=0 and OK' denote s'(error)=0. We define: