From: JP Thornley <jpt@diphi.demon.co.uk>
Subject: Re: [Spark] Converting Arrays
Date: Tue, 11 Mar 2003 20:46:20 +0000
Date: 2003-03-11T20:46:20+00:00 [thread overview]
Message-ID: <ON9GtiBcskb+IwAh@diphi.demon.co.uk> (raw)
In-Reply-To: slrnb6rfur.nq.lutz@taranis.iks-jena.de
In article <slrnb6rfur.nq.lutz@taranis.iks-jena.de>, Lutz Donnerhacke
<lutz@iks-jena.de> writes
[snip]
>
>But how can I write the required pre conditions?
>
> *******************************************************
> Listing of SPARK Text
> SPARK95 Examiner with VC and RTC Generator Release 6.3 / 11.02
> Demonstration Version
> *******************************************************
>
>
> DATE : 11-MAR-2003 11:49:13.68
>
>Line
> 1 with Kernel.Linux_i86;
> 2 --# inherit Kernel, Kernel.Linux_i86;
> 3
> 4 package Kernel.IO is
> 5 pragma Pure;
> 6
> 7 subtype long is Linux_i86.long;
> 8
> 9 type Fullpath is array(Positive range <>) of Character;
> 10 procedure To_Fullpath (s : String; path : out Fullpath);
> 11 --# derives path from s;
> 12 --# pre s'Length < path'Length;
> ^1
>*** ( 1) Semantic Error:322: Only imports may be referenced in pre-conditions
> or return expressions.
>
> 13 pragma Inline (To_Fullpath);
> 14 pragma Inline_Always (To_Fullpath);
>[...]
>5 summarised warning(s), comprising:
> 5 pragma(s)*
>(*Note: the above warnings may affect the validity of the analysis.)
>
>
>
Since you can't write it immediately, the only way is probably to
declare a proof function:
--# function Length_Of_Path return Integer;
then the precondition can be
--# pre s'Length < Length_Of_Path;
You can then write the proof rule for Length_Of_Path:
to_fullpath_rules(100): length_of_path may_be_replaced_by
path__last - path__first + 1 .
Append this to the generated rule file before running the Simplifier.
(The rule number needs to be larger than the highest rule number
generated by the Examiner).
Cheers,
Phil
--
JP Thornley
next prev parent reply other threads:[~2003-03-11 20:46 UTC|newest]
Thread overview: 18+ messages / expand[flat|nested] mbox.gz Atom feed top
2003-03-10 17:06 [Spark] Converting Arrays Lutz Donnerhacke
2003-03-10 20:03 ` James S. Rogers
2003-03-10 22:33 ` Lutz Donnerhacke
2003-03-11 10:14 ` Rod Chapman
2003-03-11 10:51 ` Lutz Donnerhacke
2003-03-11 10:52 ` Lutz Donnerhacke
2003-03-11 20:46 ` JP Thornley [this message]
2003-03-12 8:43 ` Phil Thornley
2003-03-12 11:57 ` Lutz Donnerhacke
2003-03-12 18:46 ` JP Thornley
2003-03-13 10:14 ` Lutz Donnerhacke
2003-03-12 9:43 ` Rod Chapman
2003-03-12 10:15 ` Lutz Donnerhacke
-- strict thread matches above, loose matches on Subject: below --
2003-03-13 5:55 Grein, Christoph
2003-03-13 9:47 ` Peter Amey
2003-03-13 10:15 ` Lutz Donnerhacke
2003-03-21 15:05 ` Peter Amey
2003-03-21 15:17 ` Lutz Donnerhacke
replies disabled
This is a public inbox, see mirroring instructions
for how to clone and mirror all data and code used for this inbox