From mboxrd@z Thu Jan 1 00:00:00 1970 X-Spam-Checker-Version: SpamAssassin 3.4.6 (2021-04-09) on ip-172-31-74-118.ec2.internal X-Spam-Level: X-Spam-Status: No, score=-0.5 required=3.0 tests=BAYES_05 autolearn=ham autolearn_force=no version=3.4.6 X-Received: by 2002:a05:6214:122b:: with SMTP id p11mr3150755qvv.25.1630669569624; Fri, 03 Sep 2021 04:46:09 -0700 (PDT) X-Received: by 2002:a25:540b:: with SMTP id i11mr4287541ybb.139.1630669569365; Fri, 03 Sep 2021 04:46:09 -0700 (PDT) Path: eternal-september.org!reader02.eternal-september.org!news.misty.com!border2.nntp.dca1.giganews.com!nntp.giganews.com!news-out.google.com!nntp.google.com!postnews.google.com!google-groups.googlegroups.com!not-for-mail Newsgroups: comp.lang.ada Date: Fri, 3 Sep 2021 04:46:09 -0700 (PDT) In-Reply-To: <4fc90fe9-f75e-437c-babd-05ea194d42e6n@googlegroups.com> Injection-Info: google-groups.googlegroups.com; posting-host=80.194.57.154; posting-account=xS3LTwoAAAB3aeXopC8a-M58TGE8K6go NNTP-Posting-Host: 80.194.57.154 References: <10e82e71-53f5-46d0-8960-46a7593b964dn@googlegroups.com> <86r1e80zu2.fsf@stephe-leake.org> <4fc90fe9-f75e-437c-babd-05ea194d42e6n@googlegroups.com> User-Agent: G2/1.0 MIME-Version: 1.0 Message-ID: <7df72bca-16f6-4aac-9f95-ef09cf0bbca3n@googlegroups.com> Subject: Re: Postcondition on Strings.Maps.To_Sequence From: Mark Wilson Injection-Date: Fri, 03 Sep 2021 11:46:09 +0000 Content-Type: text/plain; charset="UTF-8" Content-Transfer-Encoding: quoted-printable Xref: reader02.eternal-september.org comp.lang.ada:62617 List-Id: Good morning, It's fairly easy to prove the positive case (level 2, latest AdaCore commun= ity edition) that if a character is in a set, it's also in a sequence ---------------------------------------------------------------------------= ----- function Element (Set : in Character_Set; Value : in Character) return Boolean with Ghost, Global =3D> null, Depends =3D> (Element'Result =3D> (Set, Value)); ---------------------------------------------------------------------------= ----- function Element (Set : in Character_Set; Value : in Character) return Boolean is (Set (Value)); ---------------------------------------------------------------------------= ----- function To_Sequence (Set : in Character_Set) return Character_Sequence with Global =3D> null, Depends =3D> (To_Sequence'Result =3D> (Set)), Post =3D> (for all m in Character'Range =3D> (if Element (Set, m) then (for some n in To_Sequence'Result'Range =3D> To_Sequence'Result(n) =3D m))); ---------------------------------------------------------------------------= ----- function To_Sequence (Set : in Character_Set) return Character_Sequence is Result : String (1 .. Character'Pos (Character'Last) + 1) with Relaxed_Initialization; Count : Natural :=3D 0; begin =20 for Char in Set'Range loop =20 pragma Warnings (Off); =20 pragma Loop_Invariant (Count <=3D Character'Pos (Char)); =20 pragma Loop_Invariant (Result (Result'First .. Count)'Initialized); pragma Loop_Invariant (if Char > Set'First then (for all m in Set'First .. Character'Pred (Char) =3D> (if Element (Set, m) then (for some n in Result'First .. Count =3D> Result(n) =3D m)))); =20 pragma Warnings (On); =20 if Set(Char) then Count :=3D Count + 1; Result(Count) :=3D Char; end if; end loop; =20 return Result (1 .. Count); =20 end To_Sequence; ---------------------------------------------------------------------------= ----- The pragma Warnings (Off); are there since the Ada compiler doesn't unders= tand Relaxed_Initialization. We have to enclose the entire set of Loop_Inva= riants since Spark requires them all to be next to each other, and if we in= sert the pragma Warnings just around the 'Initialized invariant, we get war= nings. Of course, we turn them back on as soon as we can. Respectively, the loop invariants prove three things, here: (i) That count is in range (ii) That we're initializing Result as we go along (iii) If a character is in the Set, then it's in the sequence This is a *partial proof*. (At least) two more things to do here: (i) Prove that sequence is ordered - the original Ada design, whilst not sp= ecifying that the sequence is ordered, always returned it ordered, and you = know - I mean you *just* know, that someone relies on that! (ii) Prove that if a character is not in the set, then it's not in the sequ= ence This should get you going. Cheers, M