Project

General

Profile

Download (748 Bytes)

Feature #9598 ยป test.h

Denis Efremov, 04/15/2019 07:35 PM

 
typedef int value_type;

typedef unsigned int size_type;

#

/*@
inductive Count2{L}(value_type *a, integer n, value_type v, integer sum) {
case Nil{L}:
\forall value_type *a, v, integer n;
n <= 0 ==>
Count2{L}(a, n, v, 0);
case Hit{L}:
\forall value_type *a, v, integer n, sum;
0 < n && a[n-1] == v && Count2{L}(a, n-1, v, sum) ==>
Count2{L}(a, n, v, sum + 1);
case Miss{L}:
\forall value_type *a, v, integer n, sum;
0 < n && a[n-1] != v && Count2{L}(a, n-1, v, sum) ==>
Count2{L}(a, n, v, sum);
}

lemma
Count2NonNegativeSum{L}:
\forall value_type *a, v, integer n, sum;
Count2(a, n, v, sum) ==> sum >= 0;
*/

    (1-1/1)