X-Received: by 10.236.16.165 with SMTP id h25mr544311yhh.30.1409789262181; Wed, 03 Sep 2014 17:07:42 -0700 (PDT) X-Received: by 10.140.33.161 with SMTP id j30mr14759qgj.4.1409789262142; Wed, 03 Sep 2014 17:07:42 -0700 (PDT) Path: csiph.com!v102.xanadu-bbs.net!xanadu-bbs.net!news.glorb.com!peer02.iad.highwinds-media.com!news.highwinds-media.com!feed-me.highwinds-media.com!m5no5610000qaj.0!news-out.google.com!q8ni1qal.1!nntp.google.com!dc16no974088qab.1!postnews.google.com!glegroupsg2000goo.googlegroups.com!not-for-mail Newsgroups: comp.specification.misc Date: Wed, 3 Sep 2014 17:07:42 -0700 (PDT) In-Reply-To: Complaints-To: groups-abuse@google.com Injection-Info: glegroupsg2000goo.googlegroups.com; posting-host=179.219.55.88; posting-account=2anx3woAAACv_Ww98qvwud_7x0BRPyms NNTP-Posting-Host: 179.219.55.88 References: User-Agent: G2/1.0 MIME-Version: 1.0 Message-ID: <270856c9-b89b-4f3d-acd9-b8ec00cc92fb@googlegroups.com> Subject: Re: Finding loop invariants for programs that exist entirely inside loops From: Rafael Anschau Injection-Date: Thu, 04 Sep 2014 00:07:42 +0000 Content-Type: text/plain; charset=ISO-8859-1 Content-Transfer-Encoding: quoted-printable X-Received-Bytes: 2984 X-Received-Body-CRC: 1105877200 Xref: csiph.com comp.specification.misc:86 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:=20 >=20 > before the program begins, the memory has certain values; after the=20 >=20 > program ends, the memory has certain values; and the only correctness=20 >=20 > criterion is about those values. >=20 >=20 >=20 > Games and operating systems are not like that. For example, the=20 >=20 > correctness criterion of a game is all about sequences of inputs and=20 >=20 > outputs, and nothing about memory values. You may look up "model=20 >=20 > checking", "I/O automata", and "reactive systems" for how to specify and= =20 >=20 > verify programs like this. >=20 >=20 >=20 > To be sure, certain parts of a game program may work solely in terms of= =20 >=20 > memory values. These can be specified and verified by the=20 >=20 > pre/post-condition way. But these are individual parts, not the whole thi= ng. Very enlightening. I find it somewhat easy to spot those internals pre/post= conditions(depending on the problem) by asking myself what pre/post condit= ions would satisfy given specifications for the system, but was annoyed for= not being able to reason about the entire program that way. For example, o= perating systems would have the inner pre-condition that a variable has som= e specific interrupt value, and as post-condition the fact that the output = of the function triggered by the interrupt satisfies some restriction. I th= ought 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 po= inting out other more suitable formalisms.