Okay.

So,

we're in the process of understanding dynamic

program logic. The idea is that we have a

multimodal logic in which we

implement the dynamic program logic.

So, we're in the process of understanding dynamic

program logic in which we

can do programs and

assertions about termination of these programs and

what we know afterwards.

Okay, so we can say if

the program X

is assigned A

terminates, then it is true that

if Y is assigned A terminates, then it's

equal to A. And we looked at this

logic.

The idea behind the first order

version of this is that in the semantics,

the possible worlds are states,

not sets of states. Could you please share the screen?

Oh, yes, sorry. Thank you

for being quick about it.

There we go.

The idea is that

the semantics of a program

is

a multi-modal

property frame such that the states

are the possible worlds are just

variable assignments. Variable assignments

which correspond to

the current state of the variables in an imperative program

on the heap.

The thing we do when we debug

anyway, we look at the values of certain variables

which change during an imperative program.

Which is different than for a

functional program where essentially

variables are not assigned to but they're bound so they never change.

So that is a completely

different set up for variable

semantics of functional programming languages are relatively

simple. You can do that with classical logic.

For imperative programming languages, you need these

cryptic frames where the possible worlds are states.

And in these

in this interpretation,

the idea is that programs are just