Groups | Search | Server Info | Login | Register

Groups > comp.specification.misc > #86

Re: Finding loop invariants for programs that exist entirely inside loops

Show all headers | View raw

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.

Back to comp.specification.misc | Previous | Next — Previous in thread | Find similar

Thread

Finding loop invariants for programs that exist entirely inside loops Rafael Anschau <rafael.anschau@gmail.com> - 2014-08-17 11:05 -0700
  Re: Finding loop invariants for programs that exist entirely inside loops "Albert Y. C. Lai" <trebla@vex.net> - 2014-09-01 13:40 -0400
    Re: Finding loop invariants for programs that exist entirely inside loops Rafael Anschau <rafael.anschau@gmail.com> - 2014-09-03 17:07 -0700

csiph-web