From mboxrd@z Thu Jan  1 00:00:00 1970
X-Spam-Checker-Version: SpamAssassin 3.4.4 (2020-01-24) on polar.synack.me
X-Spam-Level: 
X-Spam-Status: No, score=-1.9 required=5.0 tests=BAYES_00
	autolearn=unavailable autolearn_force=no version=3.4.4
Path: 
 eternal-september.org!reader01.eternal-september.org!reader02.eternal-september.org!news.eternal-september.org!mx02.eternal-september.org!.POSTED!not-for-mail
From: Paul Rubin <no.email@nospam.invalid>
Newsgroups: comp.lang.ada
Subject: Re: {Pre,Post}conditions and side effects
Date: Tue, 12 May 2015 11:44:22 -0700
Organization: A noiseless patient Spider
Message-ID: <87y4ktzldl.fsf@jester.gateway.sonic.net>
References: <2430252d-52a1-4609-acef-684864e6ca0c@googlegroups.com>
	<AnYlw.957256$Rp.242412@fx23.iad>
	<0a718b39-ebd3-4ab5-912e-f1229679dacc@googlegroups.com>
	<wccoaqucn51.fsf@shell01.TheWorld.com>
	<9ee5e186-5aaa-4d07-9490-0f9fdbb5ca18@googlegroups.com>
	<alpine.CYG.2.11.1412231747100.4196@WIL414CHAPIN.vtc.vsc.edu>
	<wccegrpq2om.fsf@shell01.TheWorld.com>
	<87tww5296f.fsf@adaheads.sparre-andersen.dk>
	<871tj9dp5b.fsf@theworld.com>
	<ce4af31e-d491-479f-a5b3-0b3eedea2a68@googlegroups.com>
	<midvq5$2u3$1@loke.gir.dk>
	<alpine.DEB.2.11.1505071103310.14859@debian>
	<migc9a$jp8$1@loke.gir.dk>
	<alpine.DEB.2.11.1505072052570.16448@debian>
	<mijen0$1hj$1@loke.gir.dk>
	<alpine.DEB.2.11.1505111113020.12062@debian>
	<mirjho$lqh$1@loke.gir.dk>
	<alpine.DEB.2.11.1505120951500.17718@debian>
	<alpine.DEB.2.11.1505121319240.25376@debian>
Mime-Version: 1.0
Content-Type: text/plain
Injection-Info: mx02.eternal-september.org;
 posting-host="631d4aa67102f56712a7d69e4aea5bbf";
	logging-data="15470"; mail-complaints-to="abuse@eternal-september.org";
	posting-account="U2FsdGVkX18KvdN0BsucTL2cB8nuw0gT"
User-Agent: Gnus/5.13 (Gnus v5.13) Emacs/24.3 (gnu/linux)
Cancel-Lock: sha1:XoEJu1nAqSEC2fQd8jzAy4cqtIY=
	sha1:ixzxOsD0d90biE4RaAShqYv0PWA=
Xref: news.eternal-september.org comp.lang.ada:25846
Date: 2015-05-12T11:44:22-07:00
List-Id: <comp.lang.ada>

Stefan.Lucks@uni-weimar.de writes:
>   pre => (for I in 2 .. N-1 => (N mod I /=0))

Of course that still doesn't prove that N is prime: you need a separate
proof that N has no divisors greater than N, and that proof has to
quantify over all the integers, so it's not executable at all.  Stuff
like this is why formal methods are often less convenient than we'd
like.