From: Georg Bauhaus <rm.dash-bauhaus@futureapps.de>
Subject: Re: Spark_IO: improving with postconditions?
Date: Wed, 26 Aug 2009 11:23:43 +0200
Date: 2009-08-26T11:23:41+02:00 [thread overview]
Message-ID: <4a94ff1d$0$31876$9b4e6d93@newsspool3.arcor-online.net> (raw)
In-Reply-To: <a6cc46c0-eab3-4a77-b3dd-ee870d85c936@18g2000yqa.googlegroups.com>
Maciej Sobczak schrieb:
> procedure Get_Line (File : in File_Type;
> Item : out String;
> Stop : out Natural);
> --# global in out Inputs;
> --# derives Inputs,
> --# Item,
> --# Stop from Inputs, File;
> --# declare delay;
>
> Wouldn't it be good to enhance this specification with additional:
>
> --# post Stop <= Item'Last;
Will Spark accept this String?
X : String (-1 .. -2);
If so, another precodition might be needed, Item'Last in Natural;
If Get_Line (or for that matter, a program) can do useful
things with empty string buffers. Is it desirable?
next prev parent reply other threads:[~2009-08-26 9:23 UTC|newest]
Thread overview: 4+ messages / expand[flat|nested] mbox.gz Atom feed top
2009-08-26 8:57 Spark_IO: improving with postconditions? Maciej Sobczak
2009-08-26 9:23 ` Georg Bauhaus [this message]
2009-08-26 14:47 ` xavier grave
2009-08-26 15:47 ` Georg Bauhaus
replies disabled
This is a public inbox, see mirroring instructions
for how to clone and mirror all data and code used for this inbox