%%% %%% Author: Paul Y Gloess %%% http://dept-info.labri.u-bordeaux.fr/~gloess/ %%% %%% LaBRI, ENSERB & Universite Bordeaux I %%% 351, Cours de la Liberation %%% 33405 Talence Cedex %%% France %%% %%% This is a specialization of standard program verification, in the case %%% where the domain is that of integers. %%% Note November 17, 1999: we adapt JUDGEMENTs to PVS 2.3 syntax. %%% integer_program_verification: THEORY BEGIN %% These judgements don't seem to help! JUDGEMENT +(i, j: int) HAS_TYPE int JUDGEMENT -(i, j: int) HAS_TYPE int JUDGEMENT *(i, j: int) HAS_TYPE int JUDGEMENT abs(i: int) HAS_TYPE int %% %% Inequality tricks: %% mult_decompose_le: LEMMA (FORALL (a, b, c: int): a>=0 AND b>0 AND a*b=c IMPLIES a<=c) ; mult_pos_le: LEMMA (FORALL (a, b, k: int): a<=b AND k>=0 IMPLIES a*k <= b*k) ; mult_pos_le_sym: COROLLARY (FORALL (a, b, k: int): a<=b AND k>=0 IMPLIES a*k <= k*b) ; %% %% r^i is defined in the prelude when r is real and %% i is an integer such that either r /= 0 or i >= 0. %% We specify ** as a binary operator in int, which %% is the same as ^ wherever the latter is defined. [We cannot %% overload ^ here, because this would be ambiguous.] int_nat_power: LEMMA % helps existence TCC proof % [this is actually a prelude % judgement.] (FORALL (i: int, n: nat): integer_pred(i^n)) ; **(i: int, j: int) : {z : int | j >= 0 IMPLIES z = i^j} JUDGEMENT ** HAS_TYPE [int, int -> int] i_power_0: LEMMA (FORALL (i: int): i**0 = 1) ; i_power_j_0: COROLLARY (FORALL (i, j: int): j = 0 IMPLIES i**j = 1) ; power_monotonic: LEMMA % [note that 0**0=1 and 0**1=0.] (FORALL (a, b, i, j: int): a>0 AND a<=b AND 0<=i AND i<=j IMPLIES a**i <= b**j) ; power_one_le: LEMMA (FORALL (k, i, j: int): k<=i AND i>=0 AND j>=1 IMPLIES k <= i**j) ; one_less_power: LEMMA (FORALL (i, j: int): i>0 AND j>=0 IMPLIES 1 <= i**j) ; power_pos: COROLLARY (FORALL (i, j: int): i>0 AND j>=0 IMPLIES i**j > 0) ; power_minus_1: LEMMA (FORALL (i, n: int): n>0 IMPLIES i**n = i*(i**(n-1))) ; i_power_1: LEMMA (FORALL (i: int): i**1 = i) ; i_power_2: LEMMA (FORALL (i: int): i**2 = i*i) ; % square_power: LEMMA % causes a loop! % (FORALL (i: int): i*i = i**2) ; power_succ: COROLLARY (FORALL (i: int, n: nat): i**(1+n) = i*(i**n)) ; power_plus: LEMMA (FORALL (i: int, m, n: nat): i**(m+n) = (i**m)*(i**n)) ; star_power: LEMMA (FORALL (i, j: int, n: nat): (i*j)**n = (i**n)*(j**n)) ; power_power: LEMMA (FORALL (i: int, m, n: nat): (i**m)**n = i**(m*n)) ; IMPORTING standard_verification[int] %% %% Function basis: %% CONVERSION l: [int -> term] ; % 0, 1, ..., become terms! zero: constant[term] = 0 ; % not really necessary one: constant[term] = 1 ; % (see above conversion). CONVERSION l: [unary[int] -> unary[term]] abs: unary[term] = l(restrict[real, int, real](abs)) ; CONVERSION l: [binary[int] -> binary[term]] CONVERSION l: [ternary[int] -> ternary[term]] +: binary[term] = l(+) ; -: binary[term] % sometimes yields wrong TCC in "alt_minus" without "restrict". %= l(-) ; = l(restrict[[real, real], [int, int], real](-)) ; *: binary[term] = l(restrict[[real, real], [int, int], real](*)) ; **: binary[term] = l(**) ; % X**2 does not convert automatically! min: binary[term] = l(restrict[[real,real], [int, int], real](min)) ; max: binary[term] = l(restrict[[real,real], [int, int], real](max)) ; CONVERSION l: [unary[int, bool] -> unary[term, assertion]] CONVERSION l: [binary[int, bool] -> binary[term, assertion]] CONVERSION l: [ternary[int, bool] -> ternary[term, assertion]] %% %% Predicate basis: all of these, except "diff", should be automatically %% converted into their "l(...)" counterpart, but %% conversions do not always work as expected, and %% "<=" conversion yields weird TCCs (see below). %% >=: binary[term, assertion] = l(>=) ; % CONVERSION does not do it! >: binary[term, assertion] = l(>) ; % CONVERSION does not do it! <=: binary[term, assertion] = l(<=) ; % without it, weird TCCs % in "sqrt_example". <: binary[term, assertion] = l(<) ; diff: binary[term, assertion] = l(/=) ; %% %% This well founded relation in int is useful for loop termination %% arguments: %% lti:(well_founded?[int]) = (LAMBDA (m, n: int): 0 <= m AND m < n) ; %% %% Because PVS raises undue TCCs related to integer (rational %% subtype) the general "alt_dd2" rewrite rule and similar %% ones do not perform as well as expected. Hence we prove %% specialized versions: %% alt_abs: LEMMA % abs(t1)[x/t] = abs(t1[x/t]) . (FORALL (x: variable, t, t1: term): alt(x, t)(abs(t1)) = abs(alt(x, t)(t1))) ; alt_plus: LEMMA % t1+t2[x/t] = t1[x/t]+t2[x/t] . (FORALL (x: variable, t, t1, t2: term): alt(x, t)(t1 + t2) = alt(x, t)(t1) + alt(x, t)(t2)) ; alt_minus: LEMMA % t1-t2[x/t] = t1[x/t]-t2[x/t] . (FORALL (x: variable, t, t1, t2: term): alt(x, t)(t1 - t2) = alt(x, t)(t1) - alt(x, t)(t2)) ; alt_star: LEMMA % t1*t2[x/t] = t1[x/t]*t2[x/t] . (FORALL (x: variable, t, t1, t2: term): alt(x, t)(t1 * t2) = alt(x, t)(t1) * alt(x, t)(t2)) ; alt_min: LEMMA % min(t1,t2)[x/t] = min(t1[x/t],t2[x/t]) . (FORALL (x: variable, t, t1, t2: term): alt(x, t)(min(t1, t2)) = min(alt(x, t)(t1), alt(x, t)(t2))) ; alt_max: LEMMA % max(t1,t2)[x/t] = max(t1[x/t],t2[x/t]) . (FORALL (x: variable, t, t1, t2: term): alt(x, t)(max(t1, t2)) = max(alt(x, t)(t1), alt(x, t)(t2))) ; END integer_program_verification