Re: return statements in procedures

[Robert Dewar <robert_dewar@my-deja.com>]

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.