Prof. Martin Hofmann, Büchi Types
Buchi Types
(joint work with Wei Chen)
In previous work we have been using types (or rather type-and-effect
systems) to analyse the runtime behaviour of object-oriented programs and in
particular the adherence to programming guidelines and resource
consumption.
We were now trying to extend this to infinitary behaviour, ie.
specification based on w-regular languages and/or Buchi automata so as
to be able to capture fairness and liveness properties.
Perhaps surprisingly, the usual typing rule for recursive functions
does not work in this case:
Suppose that a() and b() are functions of type unit->unit that issue an
a-event, respectively a b-event. Thus, we would get an effect typing
like a() : unit & {a} and b() : unit & {b}. Now let S denote the
w-regular language (a^*b)^w, i.e. infinitely many b's and suppose that
m() is defined recursively by m(){a();m()}. With the usual typing rule
for recursion we could then justify the erroneous effect typing m():unit
& S, for assuming m():unit & S we derive a();m():aS hence a();m():S
since aS=S.
Thus, the recursive typing rule (assume any type for recursive calls
justify it for the body) is not sound for infinitary behaviours.
We have worked out the following alternative typing rule: given a
recursive definition m(){body} assume m():unit&X for a "variable" X.
Derive body:unit&AX+B for A a language of finite words and B a language
of infinite words. Conclude from this that m():unit&A^*B+A^w. This is
sound, useful, and even complete in a sense that I will make precise. In
the example from m():unit&X we conclude body:unit&aX+0 so that,
unconditionally, we get m():unit&a^w.
Artikelaktionen