Finding loop invariants for programs that exist entirely inside loops

[Rafael Anschau]

Most books say the way to find a loop invariant is by weakening the post-condition of the loop, or by finding a generalization of the pre and post-conditions of the loop. But what about games and operating systems, where everything happens inside a main loop, and where the program terminates after the end of the loop ? Are there post-condtions here suitable for finding loop invariants ? If there´re no post-condition to work with, how does one find a loop
invariant in those situations ?

Thanks,

Rafael

[Albert Y. C. Lai]

On 14-08-17 02:05 PM, Rafael Anschau wrote:
> Most books say the way to find a loop invariant is by weakening the post-condition of the loop, or by finding a generalization of the pre and post-conditions of the loop. But what about games and operating systems, where everything happens inside a main loop, and where the program terminates after the end of the loop ? Are there post-condtions here suitable for finding loop invariants ? If there´re no post-condition to work with, how does one find a loop
> invariant in those situations ?

The pre/post-condition way is designed for this kind of programs only:
before the program begins, the memory has certain values; after the
program ends, the memory has certain values; and the only correctness
criterion is about those values.

Games and operating systems are not like that. For example, the
correctness criterion of a game is all about sequences of inputs and
outputs, and nothing about memory values. You may look up "model
checking", "I/O automata", and "reactive systems" for how to specify and
verify programs like this.

To be sure, certain parts of a game program may work solely in terms of
memory values. These can be specified and verified by the
pre/post-condition way. But these are individual parts, not the whole thing.

[Rafael Anschau]

Em segunda-feira, 1 de setembro de 2014 14h40min19s UTC-3, Albert Y. C. Lai escreveu:
> The pre/post-condition way is designed for this kind of programs only:
>
> before the program begins, the memory has certain values; after the
>
> program ends, the memory has certain values; and the only correctness
>
> criterion is about those values.
>
>
>
> Games and operating systems are not like that. For example, the
>
> correctness criterion of a game is all about sequences of inputs and
>
> outputs, and nothing about memory values. You may look up "model
>
> checking", "I/O automata", and "reactive systems" for how to specify and
>
> verify programs like this.
>
>
>
> To be sure, certain parts of a game program may work solely in terms of
>
> memory values. These can be specified and verified by the
>
> pre/post-condition way. But these are individual parts, not the whole thing.

Very enlightening. I find it somewhat easy to spot those internals pre/post conditions(depending on the problem) by asking myself what pre/post conditions would satisfy given specifications for the system, but was annoyed for not being able to reason about the entire program that way. For example, operating systems would have the inner pre-condition that a variable has some specific interrupt value, and as post-condition the fact that the output of the function triggered by the interrupt satisfies some restriction. I thought I was not getting something about the pre-post method, but I am glad to know it was not designed for those kinds of systems and thank you for pointing out other more suitable formalisms.