From 0d49fb74eadcf933f696420cd182077927680d26 Mon Sep 17 00:00:00 2001 From: Nathanael Sensfelder Date: Wed, 18 Jan 2017 19:09:16 +0100 Subject: Done with 'core', starting to work on 'knowledge'. --- src/core/sequence_creation.c | 9 +++++++-- 1 file changed, 7 insertions(+), 2 deletions(-) (limited to 'src/core/sequence_creation.c') diff --git a/src/core/sequence_creation.c b/src/core/sequence_creation.c index 1133be9..f460629 100644 --- a/src/core/sequence_creation.c +++ b/src/core/sequence_creation.c @@ -19,6 +19,11 @@ * (> weights_sum 0). * (= (sum weights) weights_sum). */ +/*@ + @ requires (weights_sum > 0); + @ requires \valid(weights); + @ requires (\sum(0, (\length(weights) - 1), weights) = weights_sum); +@*/ static ZoO_index weighted_random_pick ( const ZoO_index weights [const restrict static 1], @@ -29,12 +34,12 @@ static ZoO_index weighted_random_pick accumulator = 0; - /* Safe: Included in [0, weights_sum]. */ random_number = ZoO_index_random_up_to(weights_sum); + /*@ ensures (0 <= random_number <= weights_sum); @*/ for (result = 0; accumulator < random_number; ++result) { - /* Safe: (= (sum weights) weights_sum) */ + /*@ requires (\sum(0, (\length(weights) - 1), weights) = weights_sum); @*/ accumulator += weights[result]; } -- cgit v1.2.3-70-g09d2