summaryrefslogtreecommitdiff
path: root/src/sequence/sequence.h
diff options
context:
space:
mode:
Diffstat (limited to 'src/sequence/sequence.h')
-rw-r--r--src/sequence/sequence.h175
1 files changed, 119 insertions, 56 deletions
diff --git a/src/sequence/sequence.h b/src/sequence/sequence.h
index d1ac16f..d9cbf86 100644
--- a/src/sequence/sequence.h
+++ b/src/sequence/sequence.h
@@ -18,43 +18,52 @@
requires \valid(*sequence);
requires \valid(sequence_capacity);
requires \valid(io);
- requires ((sequence_required_capacity * sizeof(ZoO_index)) <= SIZE_MAX);
- requires (*sequence_capacity >= 0);
- requires (*sequence_capacity <= SIZE_MAX);
+
requires (((*sequence_capacity) * sizeof(ZoO_index)) <= SIZE_MAX);
- requires \separated(sequence, sequence_capacity, io);
+ requires ((sequence_required_capacity * sizeof(ZoO_index)) <= SIZE_MAX);
- ensures
- (
- (
- (\result >= 0)
- && (*sequence_capacity >= sequence_required_capacity)
- && ((*sequence_capacity * sizeof(ZoO_index)) <= SIZE_MAX)
- )
- || (\result < 0)
- );
+ requires \separated(sequence, *sequence, sequence_capacity, io);
- behavior successful_reallocation:
- assigns (*sequence);
- assigns (*sequence_capacity);
+ ensures \separated(sequence, *sequence, sequence_capacity, io);
+ ensures (((*sequence_capacity) * sizeof(ZoO_index)) <= SIZE_MAX);
+ ensures ((sequence_required_capacity * sizeof(ZoO_index)) <= SIZE_MAX);
+ ensures \valid(sequence);
+ ensures \valid(*sequence);
+ ensures \valid(sequence_capacity);
+ ensures \valid(io);
- ensures (\result > 0);
- ensures ((*sequence_capacity) == sequence_required_capacity);
- ensures \valid(sequence);
+ assigns (*sequence);
+ assigns (*sequence_capacity);
- behavior already_done:
- assigns \nothing;
+ ensures ((\result == 1) || (\result == 0) || (\result == -1));
- ensures (\result == 0);
- ensures ((*sequence_capacity) >= sequence_required_capacity);
+ ensures
+ (
+ (\result == 1) ==>
+ ((*sequence_capacity) == sequence_required_capacity)
+ );
- behavior failure:
- assigns \nothing;
+ ensures
+ (
+ (\result == 1) ==>
+ ((*sequence_capacity) > \old(*sequence_capacity))
+ );
- ensures (\result < 0);
+ ensures ((\result == -1) ==> ((*sequence) == \old(*sequence)));
- complete behaviors;
- disjoint behaviors;
+ ensures
+ (
+ (\result == -1) ==>
+ ((*sequence_capacity) == \old(*sequence_capacity))
+ );
+
+ ensures ((\result == 0) ==> ((*sequence) == \old(*sequence)));
+
+ ensures
+ (
+ (\result == 0) ==>
+ ((*sequence_capacity) == \old(*sequence_capacity))
+ );
@*/
int ZoO_sequence_ensure_capacity
(
@@ -109,30 +118,58 @@ int ZoO_sequence_create_from
);
/*@
+ requires \valid(sequence);
+ requires \valid(*sequence);
+ requires \valid(sequence_capacity);
requires \valid(sequence_length);
requires \valid(io);
requires (((*sequence_length) * sizeof(ZoO_index)) <= SIZE_MAX);
requires (((*sequence_capacity) * sizeof(ZoO_index)) <= SIZE_MAX);
- requires \separated(sequence, sequence_capacity, sequence_length, io);
+ requires \separated(sequence, sequence, sequence_capacity, sequence_length, io);
- behavior success:
- assigns (*sequence_length);
- assigns (*sequence[0]);
- assigns (*sequence_capacity);
+ assigns (*sequence_length);
+ assigns (*sequence[0]);
+ assigns (*sequence_capacity);
- ensures (\result >= 0);
- ensures ((*sequence_length > \old(*sequence_length)));
+ ensures \valid(sequence);
+ ensures \valid(sequence_capacity);
+ ensures \valid(sequence_length);
+ ensures \valid(io);
+ ensures (((*sequence_length) * sizeof(ZoO_index)) <= SIZE_MAX);
+ ensures (((*sequence_capacity) * sizeof(ZoO_index)) <= SIZE_MAX);
+ ensures \separated(sequence, *sequence, sequence_capacity, sequence_length, io);
- behavior could_not_increase_length:
- ensures (\result == -1);
+ ensures ((\result == 0) || (\result == -1));
- assigns (*sequence_length);
+ ensures
+ (
+ (\result == 0) ==>
+ (*sequence_length == (\old(*sequence_length) + 1))
+ );
- behavior could_not_reallocate:
- ensures (\result < -1);
+ ensures
+ (
+ (\result == 0) ==>
+ ((*sequence_capacity) >= \old(*sequence_capacity))
+ );
+
+ ensures ((\result == 0) ==> (*sequence_length > \old(*sequence_length)));
+
+ ensures ((\result == -1) ==> ((*sequence_length) == \old(*sequence_length)));
+ ensures ((\result == -1) ==> ((*sequence[0]) == \old(*sequence[0])));
+ ensures
+ (
+ (\result == -1) ==>
+ ((*sequence_capacity) == \old(*sequence_capacity))
+ );
+
+ ensures ((\result == -1) ==> ((*sequence_length) == \old(*sequence_length)));
+ ensures
+ (
+ (\result == -1) ==>
+ ((*sequence_capacity) == \old(*sequence_capacity))
+ );
- complete behaviors;
- disjoint behaviors;
@*/
int ZoO_sequence_append_left
(
@@ -144,32 +181,58 @@ int ZoO_sequence_append_left
);
/*@
+ requires \valid(sequence);
requires \valid(*sequence);
requires \valid(sequence_capacity);
requires \valid(sequence_length);
requires \valid(io);
requires (((*sequence_length) * sizeof(ZoO_index)) <= SIZE_MAX);
requires (((*sequence_capacity) * sizeof(ZoO_index)) <= SIZE_MAX);
- requires \separated(sequence, sequence_capacity, sequence_length, io);
+ requires \separated(sequence, sequence, sequence_capacity, sequence_length, io);
+
+ assigns (*sequence_length);
+ assigns (*sequence[0]);
+ assigns (*sequence_capacity);
- behavior success:
- assigns (*sequence_length);
- assigns (*sequence);
- assigns (*sequence_capacity);
+ ensures \valid(sequence);
+ ensures \valid(sequence_capacity);
+ ensures \valid(sequence_length);
+ ensures \valid(io);
+ ensures (((*sequence_length) * sizeof(ZoO_index)) <= SIZE_MAX);
+ ensures (((*sequence_capacity) * sizeof(ZoO_index)) <= SIZE_MAX);
+ ensures \separated(sequence, *sequence, sequence_capacity, sequence_length, io);
- ensures (\result >= 0);
- ensures ((*sequence_length > \old(*sequence_length)));
+ ensures ((\result == 0) || (\result == -1));
- behavior could_not_increase_length:
- ensures (\result == -1);
+ ensures
+ (
+ (\result == 0) ==>
+ (*sequence_length == (\old(*sequence_length) + 1))
+ );
+
+ ensures
+ (
+ (\result == 0) ==>
+ ((*sequence_capacity) >= \old(*sequence_capacity))
+ );
- assigns (*sequence_length);
+ ensures ((\result == 0) ==> (*sequence_length > \old(*sequence_length)));
- behavior could_not_reallocate:
- ensures (\result < -1);
+ ensures ((\result == -1) ==> ((*sequence_length) == \old(*sequence_length)));
+ ensures ((\result == -1) ==> ((*sequence[0]) == \old(*sequence[0])));
+ ensures
+ (
+ (\result == -1) ==>
+ ((*sequence_capacity) == \old(*sequence_capacity))
+ );
+
+ ensures ((\result == -1) ==> ((*sequence_length) == \old(*sequence_length)));
+ ensures
+ (
+ (\result == -1) ==>
+ ((*sequence_capacity) == \old(*sequence_capacity))
+ );
- complete behaviors;
- disjoint behaviors;
@*/
int ZoO_sequence_append_right
(