Groups | Search | Server Info | Login | Register

Groups > comp.specification.misc > #84

Finding loop invariants for programs that exist entirely inside loops

Show all headers | View raw

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

Back to comp.specification.misc | Previous | Next — Next 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