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
Presenters
Zugänglich über
Offener Zugang
Dauer
01:31:23 Min
Aufnahmedatum
2024-01-30
Hochgeladen am
2024-01-30 16:56:04
Sprache
en-US