0
$\begingroup$

I have been following the course Concrete Semantics with Isabelle/HOL. At some point we are given the task to verify a program/extend some semantic construction/prove some mathematical fact. I personally prefer to dive a little bit more into operational semantics, so adding new features to the IMP language is the way to go.

The classical extensions are non-determinism/parallel execution. These are described in a variety of books (Winskel, Hennessy or Nielson to cite only classical authors). However, I feel the treatment is rather limited and I'm not sure that can be turned into project, it looks more like a bunch of exercises.

So my question is are you aware of any simple but interesting extensions of the operational semantics approach to the study of a simple WHILE-program (such as IMP)? I would be looking specially for significant properties that can be proved in that semantics and illustrative examples that may be relevant.

$\endgroup$
1
  • $\begingroup$ This question is a bit broad for CS.SE. Here we prefer questions having a definite answer. Still, it shows some effort, so I'm not going to vote-close it (but I wouldn't be surprised if others are). $\endgroup$
    – chi
    Dec 20, 2018 at 12:02

1 Answer 1

1
$\begingroup$

You could add more flow control to IMP, like (simple) exceptions, or break to exit early from a while loop.

You could some partial operators (division, square root) requiring you to handle runtime errors.

You could add more complex data types, like pairs. Make it so that e.g. projecting a value out of a non-pair value causes a runtime error. Craft a (first-order) simple type system e.g. using T ::= int | (T*T) as types, and prove that "typeable programs do not go wrong", i.e. executing them never lead to runtime errors.

You could add functions / procedures. This is not so trivial at first, especially if you want to consider several ways for parameter passing (e.g. pass-by-value, pass-by-reference).

You could prove that a suitable restriction of IMP (say, sans while, or with a constrained while) is always terminating.

$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge that you have read and understand our privacy policy and code of conduct.

Not the answer you're looking for? Browse other questions tagged or ask your own question.