Re: Code safety and information hiding

[Maciej Sobczak <no.spam@no.spam.com>]

Stuart wrote:

> Rod's distinction between detail and information is a good one.  It should 
> also be remembered that the objective of SPARK is to allow you to reason 
> about what your program will do.  Often, in less rigorous design processes, 
> you might assume that a subprogram you use has no unexpected consequences 
> (e.g. side-effects).  SPARK is much more rigorous - it makes sure that 
> subprograms have no side-effects: the consequence is that _all_ effects of a 
> subprogram must be recorded (e.g. updating the Seed in the Random number 
> example).

I understand it. It's clear to me now that the spec should declare any 
interaction of the given subprogram with its environment and global 
variables are part of it - but it also became clear that with adding 
'global' annotations the network of known and checked dependencies is 
getting much denser. It's this density of dependencies that has struck 
me at the beginning.


-- 
Maciej Sobczak : http://www.msobczak.com/
Programming    : http://www.msobczak.com/prog/