Rocksolid Light

Welcome to novaBBS (click a section below)

mail  files  register  newsreader  groups  login

Message-ID:  

:-) your own self. -- Larry Wall in <199709261754.KAA23761@wall.org>


devel / comp.lang.ada / Re: Postcondition on Strings.Maps.To_Sequence

SubjectAuthor
* Postcondition on Strings.Maps.To_Sequencemockturtle
`* Re: Postcondition on Strings.Maps.To_SequenceStephen Leake
 +* Re: Postcondition on Strings.Maps.To_Sequencemockturtle
 |`* Re: Postcondition on Strings.Maps.To_SequenceMark Wilson
 | `- Re: Postcondition on Strings.Maps.To_SequenceMark Wilson
 `- Re: Postcondition on Strings.Maps.To_SequenceMark Wilson

1
Postcondition on Strings.Maps.To_Sequence

<10e82e71-53f5-46d0-8960-46a7593b964dn@googlegroups.com>

 copy mid

https://www.novabbs.com/devel/article-flat.php?id=5749&group=comp.lang.ada#5749

 copy link   Newsgroups: comp.lang.ada
X-Received: by 2002:a05:6214:922:: with SMTP id dk2mr18213866qvb.36.1630229928064;
Sun, 29 Aug 2021 02:38:48 -0700 (PDT)
X-Received: by 2002:a25:bc10:: with SMTP id i16mr16229962ybh.73.1630229927833;
Sun, 29 Aug 2021 02:38:47 -0700 (PDT)
Path: i2pn2.org!i2pn.org!weretis.net!feeder8.news.weretis.net!proxad.net!feeder1-2.proxad.net!209.85.160.216.MISMATCH!news-out.google.com!nntp.google.com!postnews.google.com!google-groups.googlegroups.com!not-for-mail
Newsgroups: comp.lang.ada
Date: Sun, 29 Aug 2021 02:38:47 -0700 (PDT)
Injection-Info: google-groups.googlegroups.com; posting-host=217.56.127.6; posting-account=9fwclgkAAAD6oQ5usUYhee1l39geVY99
NNTP-Posting-Host: 217.56.127.6
User-Agent: G2/1.0
MIME-Version: 1.0
Message-ID: <10e82e71-53f5-46d0-8960-46a7593b964dn@googlegroups.com>
Subject: Postcondition on Strings.Maps.To_Sequence
From: framefri...@gmail.com (mockturtle)
Injection-Date: Sun, 29 Aug 2021 09:38:48 +0000
Content-Type: text/plain; charset="UTF-8"
 by: mockturtle - Sun, 29 Aug 2021 09:38 UTC

Dear.all,
in a code that I am trying to prove with SPARK I have the following two consecutive lines [I am a beginner with SPARK and I am trying to learn... it is quite fun, if you have masochistic tendencies... ;-)]

pragma Assert (Edge.On_Input /= Null_Set);
pragma Assert (To_Sequence (Edge.On_Input)'Length > 0);

where On_Input is a Character_Set (from Ada.Strings.Maps).
SPARK accepts the first (that is, it can prove that On_Input is not empty), but complains that cannot prove the second (that is, that the same set converted to string can give an empty string). Actually, the contract of To_Sequence looks like

function To_Sequence (Set : Character_Set) return Character_Sequence with
Post =>
(if Set = Null_Set then To_Sequence'Result'Length = 0)
and then
(for all Char in Character =>
(if Is_In (Char, Set)
then (for some X of To_Sequence'Result => Char = X)))
and then
(for all Char of To_Sequence'Result => Is_In (Char, Set))
and then
(for all J in To_Sequence'Result'Range =>
(for all K in To_Sequence'Result'Range =>
(if J /= K
then To_Sequence'Result (J) /= To_Sequence'Result (K))));

and it shows clearly that if the input is Null_Set, then the output is the empty string, but does no explicit claim about the opposite case (if the input is not empty, then the output is not empty as well).

My question is: is this problem due to just a "weak" contract of To_Sequence or can actually To_Sequence return the empty string for some non Null_Set input?

Re: Postcondition on Strings.Maps.To_Sequence

<86r1e80zu2.fsf@stephe-leake.org>

 copy mid

https://www.novabbs.com/devel/article-flat.php?id=5779&group=comp.lang.ada#5779

 copy link   Newsgroups: comp.lang.ada
Path: i2pn2.org!i2pn.org!aioe.org!9CzwYWWlKVx8RMZd/VcwFg.user.46.165.242.75.POSTED!not-for-mail
From: stephen_...@stephe-leake.org (Stephen Leake)
Newsgroups: comp.lang.ada
Subject: Re: Postcondition on Strings.Maps.To_Sequence
Date: Wed, 01 Sep 2021 14:07:33 -0700
Organization: Aioe.org NNTP Server
Message-ID: <86r1e80zu2.fsf@stephe-leake.org>
References: <10e82e71-53f5-46d0-8960-46a7593b964dn@googlegroups.com>
Mime-Version: 1.0
Content-Type: text/plain
Injection-Info: gioia.aioe.org; logging-data="29840"; posting-host="9CzwYWWlKVx8RMZd/VcwFg.user.gioia.aioe.org"; mail-complaints-to="abuse@aioe.org";
User-Agent: Gnus/5.13 (Gnus v5.13) Emacs/28.0.50 (windows-nt)
Cancel-Lock: sha1:1gqdGx8cEVXbVT3RtQQCBBYYlvI=
X-Notice: Filtered by postfilter v. 0.9.2
 by: Stephen Leake - Wed, 1 Sep 2021 21:07 UTC

mockturtle <framefritti@gmail.com> writes:

> pragma Assert (Edge.On_Input /= Null_Set);
> pragma Assert (To_Sequence (Edge.On_Input)'Length > 0);
>
> where On_Input is a Character_Set (from Ada.Strings.Maps).
> SPARK accepts the first (that is, it can prove that On_Input is not
> empty), but complains that cannot prove the second (that is, that the
> same set converted to string can give an empty string).

<snip>

I have used Spark some, but am not an expert.

So just guessing; does Spark actually understand 'Length?

For example, can it prove "a"'Length = 1?
and then To_Sequence (To_Set ('a'))'Length = 1?

> My question is: is this problem due to just a "weak" contract of
> To_Sequence or can actually To_Sequence return the empty string for some
> non Null_Set input?

My guess is neither; Spark is simply not smart enough yet. You'll have
to add some additional intermediate assertions in the body of
To_Sequence, especially one that relates the size of On_Input to the
size of the result string.

--
-- Stephe

Re: Postcondition on Strings.Maps.To_Sequence

<4fc90fe9-f75e-437c-babd-05ea194d42e6n@googlegroups.com>

 copy mid

https://www.novabbs.com/devel/article-flat.php?id=5787&group=comp.lang.ada#5787

 copy link   Newsgroups: comp.lang.ada
X-Received: by 2002:a05:622a:394:: with SMTP id j20mr4591033qtx.196.1630610247233;
Thu, 02 Sep 2021 12:17:27 -0700 (PDT)
X-Received: by 2002:a05:6902:1247:: with SMTP id t7mr5988216ybu.161.1630610246956;
Thu, 02 Sep 2021 12:17:26 -0700 (PDT)
Path: i2pn2.org!i2pn.org!weretis.net!feeder8.news.weretis.net!proxad.net!feeder1-2.proxad.net!209.85.160.216.MISMATCH!news-out.google.com!nntp.google.com!postnews.google.com!google-groups.googlegroups.com!not-for-mail
Newsgroups: comp.lang.ada
Date: Thu, 2 Sep 2021 12:17:26 -0700 (PDT)
In-Reply-To: <86r1e80zu2.fsf@stephe-leake.org>
Injection-Info: google-groups.googlegroups.com; posting-host=93.41.3.120; posting-account=9fwclgkAAAD6oQ5usUYhee1l39geVY99
NNTP-Posting-Host: 93.41.3.120
References: <10e82e71-53f5-46d0-8960-46a7593b964dn@googlegroups.com> <86r1e80zu2.fsf@stephe-leake.org>
User-Agent: G2/1.0
MIME-Version: 1.0
Message-ID: <4fc90fe9-f75e-437c-babd-05ea194d42e6n@googlegroups.com>
Subject: Re: Postcondition on Strings.Maps.To_Sequence
From: framefri...@gmail.com (mockturtle)
Injection-Date: Thu, 02 Sep 2021 19:17:27 +0000
Content-Type: text/plain; charset="UTF-8"
 by: mockturtle - Thu, 2 Sep 2021 19:17 UTC

On Wednesday, September 1, 2021 at 11:07:41 PM UTC+2, Stephen Leake wrote:

>
> So just guessing; does Spark actually understand 'Length?

I think it does, since I use it frequently in contracts (e.g. putting in some procedure the pre-condition that a string must be shorter than Positive'Last since otherwise Spark complains that I could have an overflow)

>
> For example, can it prove "a"'Length = 1?
> and then To_Sequence (To_Set ('a'))'Length = 1?

Good idea, I'll try this test.

Re: Postcondition on Strings.Maps.To_Sequence

<7df72bca-16f6-4aac-9f95-ef09cf0bbca3n@googlegroups.com>

 copy mid

https://www.novabbs.com/devel/article-flat.php?id=5796&group=comp.lang.ada#5796

 copy link   Newsgroups: comp.lang.ada
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: i2pn2.org!i2pn.org!weretis.net!feeder6.news.weretis.net!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: markwil...@wilsonnet.technology (Mark Wilson)
Injection-Date: Fri, 03 Sep 2021 11:46:09 +0000
Content-Type: text/plain; charset="UTF-8"
Content-Transfer-Encoding: quoted-printable
Lines: 112
 by: Mark Wilson - Fri, 3 Sep 2021 11:46 UTC

Good morning,

It's fairly easy to prove the positive case (level 2, latest AdaCore community 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 => null,
Depends => (Element'Result => (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 => null,
Depends => (To_Sequence'Result => (Set)),
Post => (for all m in Character'Range =>
(if Element (Set, m) then
(for some n in To_Sequence'Result'Range =>
To_Sequence'Result(n) = 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 := 0;
begin

for Char in Set'Range loop

pragma Warnings (Off);

pragma Loop_Invariant
(Count <= Character'Pos (Char));

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) =>
(if Element (Set, m) then
(for some n in Result'First .. Count =>
Result(n) = m))));

pragma Warnings (On);

if Set(Char) then
Count := Count + 1;
Result(Count) := Char;
end if;

end loop;

return Result (1 .. Count);

end To_Sequence;

--------------------------------------------------------------------------------

The pragma Warnings (Off); are there since the Ada compiler doesn't understand Relaxed_Initialization. We have to enclose the entire set of Loop_Invariants since Spark requires them all to be next to each other, and if we insert the pragma Warnings just around the 'Initialized invariant, we get warnings.

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 specifying 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 sequence

This should get you going.

Cheers,
M

Re: Postcondition on Strings.Maps.To_Sequence

<1f2990ab-ee11-4f6e-8541-460e0b6bc6c8n@googlegroups.com>

 copy mid

https://www.novabbs.com/devel/article-flat.php?id=5797&group=comp.lang.ada#5797

 copy link   Newsgroups: comp.lang.ada
X-Received: by 2002:a05:620a:15e8:: with SMTP id p8mr2930263qkm.27.1630669981230;
Fri, 03 Sep 2021 04:53:01 -0700 (PDT)
X-Received: by 2002:a5b:142:: with SMTP id c2mr4133996ybp.425.1630669981104;
Fri, 03 Sep 2021 04:53:01 -0700 (PDT)
Path: i2pn2.org!i2pn.org!weretis.net!feeder6.news.weretis.net!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:53:00 -0700 (PDT)
In-Reply-To: <7df72bca-16f6-4aac-9f95-ef09cf0bbca3n@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>
<7df72bca-16f6-4aac-9f95-ef09cf0bbca3n@googlegroups.com>
User-Agent: G2/1.0
MIME-Version: 1.0
Message-ID: <1f2990ab-ee11-4f6e-8541-460e0b6bc6c8n@googlegroups.com>
Subject: Re: Postcondition on Strings.Maps.To_Sequence
From: markwil...@wilsonnet.technology (Mark Wilson)
Injection-Date: Fri, 03 Sep 2021 11:53:01 +0000
Content-Type: text/plain; charset="UTF-8"
Lines: 0
 by: Mark Wilson - Fri, 3 Sep 2021 11:53 UTC

You'll also need to prove that each character in the sequence is unique ...

Re: Postcondition on Strings.Maps.To_Sequence

<4b5164f1-71da-4581-8e02-2480e24520b9n@googlegroups.com>

 copy mid

https://www.novabbs.com/devel/article-flat.php?id=5798&group=comp.lang.ada#5798

 copy link   Newsgroups: comp.lang.ada
X-Received: by 2002:a05:6214:1cb:: with SMTP id c11mr3215476qvt.47.1630670730078;
Fri, 03 Sep 2021 05:05:30 -0700 (PDT)
X-Received: by 2002:a5b:58e:: with SMTP id l14mr4694057ybp.143.1630670729857;
Fri, 03 Sep 2021 05:05:29 -0700 (PDT)
Path: i2pn2.org!i2pn.org!weretis.net!feeder6.news.weretis.net!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 05:05:29 -0700 (PDT)
In-Reply-To: <86r1e80zu2.fsf@stephe-leake.org>
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>
User-Agent: G2/1.0
MIME-Version: 1.0
Message-ID: <4b5164f1-71da-4581-8e02-2480e24520b9n@googlegroups.com>
Subject: Re: Postcondition on Strings.Maps.To_Sequence
From: markwil...@wilsonnet.technology (Mark Wilson)
Injection-Date: Fri, 03 Sep 2021 12:05:30 +0000
Content-Type: text/plain; charset="UTF-8"
Lines: 71
 by: Mark Wilson - Fri, 3 Sep 2021 12:05 UTC

On Wednesday, September 1, 2021 at 10:07:41 PM UTC+1, Stephen Leake wrote:
> My guess is neither; Spark is simply not smart enough yet. You'll have
> to add some additional intermediate assertions in the body of
> To_Sequence, especially one that relates the size of On_Input to the
> size of the result string.

No problem at all reasoning about Lengths in Spark. Here, we add the postcondition that if the result has a length of zero then the set is empty, too.

--------------------------------------------------------------------------------

function To_Sequence
(Set : in Character_Set)
return Character_Sequence
with
Global => null,
Depends => (To_Sequence'Result => (Set)),
Post => ((if To_Sequence'Result'Length = 0 then
(for all k in Character'Range =>
Element (Set, k) = False)) and
(for all m in Character'Range =>
(if Element (Set, m) then
(for some n in To_Sequence'Result'Range =>
To_Sequence'Result(n) = 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 := 0;
begin

for Char in Set'Range loop

pragma Warnings (Off);

pragma Loop_Invariant
(Count <= Character'Pos (Char));

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) =>
(if Element (Set, m) then
(for some n in Result'First .. Count =>
Result(n) = m))));

pragma Loop_Invariant
(if Result'Length = 0 then
(for all k in Set'First .. Char =>
Set(k) = False));

pragma Warnings (On);

if Set(Char) then
Count := Count + 1;
Result(Count) := Char;
end if;

end loop;

return Result (1 .. Count);

end To_Sequence;

--------------------------------------------------------------------------------

1
server_pubkey.txt

rocksolid light 0.9.7
clearnet tor