diff --git a/examples/array_most_frequent.mlw b/examples/array_most_frequent.mlw new file mode 100644 index 0000000000000000000000000000000000000000..8690537f8802a4c485af18865fdd5e18d4f59859 --- /dev/null +++ b/examples/array_most_frequent.mlw @@ -0,0 +1,33 @@ + +use int.Int +use ref.Refint +use array.Array +use array.NumOfEq + +(** A simple programming exercise: find out the most frequent value in an array + + Using an external table (e.g. a hash table), we can easily do it + in linear time and space. + + However, if the array is sorted, we can do it in linear time and + constant space. *) + +let most_frequent (a: array int) : int + requires { length a > 0 } + requires { forall i j. 0 <= i <= j < length a -> a[i] <= a[j] } + ensures { numof a result 0 (length a) > 0 } + ensures { forall x. numof a x 0 (length a) <= numof a result 0 (length a) } += let ref r = a[0] in + let ref c = 1 in + let ref m = 1 in + for i = 1 to length a - 1 do + invariant { c = numof a a[i-1] 0 i } + invariant { m = numof a r 0 i } + invariant { forall x. numof a x 0 i <= m } + if a[i] = a[i-1] then begin + incr c; + if c > m then begin m <- c; r <- a[i] end + end else + c <- 1 + done; + r diff --git a/examples/array_most_frequent/why3session.xml b/examples/array_most_frequent/why3session.xml new file mode 100644 index 0000000000000000000000000000000000000000..e69e35c94229ea83c001267649e733e28e4ae6ee --- /dev/null +++ b/examples/array_most_frequent/why3session.xml @@ -0,0 +1,75 @@ + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + diff --git a/examples/array_most_frequent/why3shapes.gz b/examples/array_most_frequent/why3shapes.gz new file mode 100644 index 0000000000000000000000000000000000000000..105d82359614f79f453456ef5d5aa1cf2f014dac Binary files /dev/null and b/examples/array_most_frequent/why3shapes.gz differ