From: r_c_chapman@my-deja.com
Subject: Re: return statements in procedures
Date: 2000/06/05
Date: 2000-06-05T00:00:00+00:00 [thread overview]
Message-ID: <8hfujg$nl5$1@nnrp1.deja.com> (raw)
In-Reply-To: 393B2054.618F6E80@baesystems.com.au
In article <393B2054.618F6E80@baesystems.com.au>,
Matthew Daniel <matthew.daniel@baesystems.com.au> wrote:
> Hi,
>
> we are having a "discussion" at work at the moment about return
> statements in procedures.
For what's it worth, they're not allowed in SPARK, and I don't
really miss them. I can only think of one or two occasions in the
last 5 years when I've really needed such a thing. 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..
- Rod Chapman
SPARK Team, Praxis Critical Systems, rod@praxis-cs.co.uk
Sent via Deja.com http://www.deja.com/
Before you buy.
next prev parent reply other threads:[~2000-06-05 0:00 UTC|newest]
Thread overview: 10+ messages / expand[flat|nested] mbox.gz Atom feed top
2000-06-05 0:00 return statements in procedures Matthew Daniel
2000-06-05 0:00 ` Ted Dennison
2000-06-05 0:00 ` r_c_chapman [this message]
2000-06-05 0:00 ` Robert Dewar
2000-06-05 0:00 ` Robert Dewar
2000-06-05 0:00 ` Geoff Bull
2000-06-06 0:00 ` Robert A Duff
2000-06-05 0:00 ` Marin D. Condic
2000-06-06 0:00 ` Geoff Bull
2000-06-06 0:00 ` Marin D. Condic
replies disabled
This is a public inbox, see mirroring instructions
for how to clone and mirror all data and code used for this inbox