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.3 required=5.0 tests=BAYES_00,INVALID_MSGID,
	MSGID_RANDY autolearn=no autolearn_force=no version=3.4.4
X-Google-Language: ENGLISH,ASCII-7-bit
X-Google-Thread: 103376,9e90e30a519a635b
X-Google-Attributes: gid103376,public
From: Robert Dewar <robert_dewar@my-deja.com>
Subject: Re: return statements in procedures
Date: 2000/06/05
Message-ID: <8hg6mq$t3m$1@nnrp1.deja.com>#1/1
X-Deja-AN: 631247226
References: <393B2054.618F6E80@baesystems.com.au>
 <8hfujg$nl5$1@nnrp1.deja.com>
X-Http-Proxy: 1.0 x57.deja.com:80 (Squid/1.1.22) for client 205.232.38.14
Organization: Deja.com - Before you buy.
X-Article-Creation-Date: Mon Jun 05 12:33:30 2000 GMT
X-MyDeja-Info: XMYDJUIDrobert_dewar
Newsgroups: comp.lang.ada
X-Http-User-Agent: Mozilla/4.61 [en] (OS/2; I)
Date: 2000-06-05T00:00:00+00:00
List-Id: <comp.lang.ada>

In article <8hfujg$nl5$1@nnrp1.deja.com>,
  r_c_chapman@my-deja.com wrote:
> The restricitons
> on return statements in SPARK are such that subprograms always
> have a single-entry/single-exit flow graph, which makes
> subsequent Flow Analysis and Verificaiton Condition Generation
> much easier..


Fair enough, but this is at the expense of human readability.
Yes, in SPARK that tradeoff often makes sense, many of the
restrictions in SPARK result in programs that are harder to
read for a human, but we have different objectives in mind
in this context :-)


Sent via Deja.com http://www.deja.com/
Before you buy.