mirror of
https://github.com/AdaCore/spark2014.git
synced 2026-02-12 12:39:11 -08:00
14 lines
415 B
Ada
14 lines
415 B
Ada
package Loop_Entry
|
|
is
|
|
|
|
subtype ElementType is Natural range 0..1000;
|
|
subtype IndexType is Positive range 1..100;
|
|
type ArrayType is array (IndexType) of ElementType;
|
|
|
|
procedure Clear (A: in out ArrayType; L,U: in IndexType);
|
|
--# derives A from A, L, U;
|
|
--# post (for all N in IndexType range L..U => (A(N) = 0)) and
|
|
--# (for all N in IndexType => ((N<L or N>U) -> A(N) = A~(N)));
|
|
|
|
end Loop_Entry;
|