I guess we can start.

So right, this is just copy and paste from the last slide of the previous lecture.

So if you recall, I gave you an example of a simple annotated program.

It was this factorial thing and in that material, in that example we have rules for assignments,

sequencing, consequence and while loops.

So we convince ourselves kind of that we have some system which can be used for annotating

programs.

Modulo, of course, is business of having to deal somehow with arithmetical statements.

And I finished the last lecture with the question of relative completeness.

So I show you that our rules can be used for something, however easy this example was.

But now we want to convince ourselves that the rules are as general as possible if we

assume that we have an oracle for arithmetic.

And I think that I mentioned briefly this notion of weakest, in this case, liberal precondition.

So again, we call that our extended notion of states consists of ordinary states and

the non-terminating ones.

And now let's say that capital, semantic weakest, liberal precondition for a given command and

a given assertion, so postcondition, is just a collection of all those extended states

which are such that after the execution of our command on this state, so if this state

happens to be bottom and non-terminating state, of course, this thing is also bottom, such

that the postcondition holds after the, the postcondition B holds after the execution

of our command on this state.

So actually this definition I could give in this very same form, however I was talking

of weakest liberal precondition or original notion of total or of weakest precondition,

which can basically preconditions in the extra sense.

And with the only difference then that the, now we have the convention that bottom forces

all assertion and in the extra condition bottom forces no assertion, all of them are false

at bottom, non-terminating pseudo state.

So this means that if we're talking about, once again it's the same distinction that

we could make in the case of hard triples themselves.

So either we could insist that hard triple is valid in a given state only if program

terminates after execution of a command in this state and then the postcondition is valid.

This would be total notion that was not central for us.

Or like here we could say that hard triple is valid in a given state if whenever a program

terminates, assuming that the program terminates at all, then postcondition be satisfied.

So if it doesn't, if it does not terminate then the hard triple then in this partial

sense is trivially valid.

And this notion of weakest liberal of this WLP corresponds to this second partial or

liberal leading of correctness assertions.

So in fact we could define semantic, why I'm talking again about hard triples?

Well because weakest precondition provide, this call machinery of weakest precondition

would provide alternative way of doing reasoning about program correctness to that of hard

triples.

In fact we could then define the validity of a hard triple in terms of this WLP.

So a triple is valid if the under a given interpretation of logical variables, if the

set of those states which make our assertion valid under this fixed interpretation of program

variables is contained in this semantic weakest liberal precondition.

So this way of doing semantics is sometimes called predicate transformer semantics.

So this is this capital WLP, sorry we have it here as well, was something defined semantically

as a set of states.

So what we would like to have then on syntactic level would be some kind of a function which