Re: Ada2012 Invariants and obaque types

["Dmitry A. Kazakov" <mailbox@dmitry-kazakov.de>]

On Tue, 21 Jun 2011 15:29:22 +0200, Georg Bauhaus wrote:

> On 21.06.11 14:31, Dmitry A. Kazakov wrote:
> 
>>> In another theory, the invariant may express things
>>> such as
>>>  Num_Green_Lights (T1) >= 3;
>>> or
>>> 'Length < State_of_Things (T1) * 2;
>>> where Num_Green_Lights is a publicly visible function whose
>>> result is somehow computed.  These predicates would be informative,
>>> and formal.
>> 
>> That is not an invariant, but a constraint.
> 
> I don't see bounds in the above.

Constraint could be any, not only bounds. It is not the formula, but the
meaning of:

   S = { x | x in T and P (x) }

here P is a constraint, which produces S.

   x in S => Q (x)

here Q is an invariant of S. It might happen that Q (x) <=> P (x). Then you
could define S using Q, that would make Q constraint and P invariant.

> That is, if the (theoretical) assertion is "at least,
> no matter what, under all circumstances, in each implementation",
> isn't this an invariant?

1. Different implementations of the same specification may have different
invariants. That are the predicates which cannot be derived from the
specification.

2. When a predicate can be derived from the specification that does not yet
imply its equivalence to the specification. Invariant does not necessarily
defines the type.

3. The difference is the intent. The specification defines the [sub]type.
Invariant merely is a predicate provable true for the given implementation
of the specification. (Properly constructed invariants can be used in
construction of implementations, e.g. Dijkstra's approach to programming,
loop invariants etc)

4. You cannot distinguish predicates used in definitions from ones used in
proofs by just looking at them. It is the language's task to do this by
syntax means.

-- 
Regards,
Dmitry A. Kazakov
http://www.dmitry-kazakov.de