[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
Re: integer_pred and mailing list
> The following is a TCC that was not automatically discharged. It seems
> to be saying "prove that the results of these operations is an integer"
> but I'm not sure what the integer_pred bit means and what I can do with
> it.
integer_pred is a predefined predicate that will return true if
the argument is an integer. Your interpretation of the TCC is
correct.
> sum_TCC1: OBLIGATION
> (FORALL (a: int, b: int, uId: [int, int]):
> a = PROJ_1(uId) AND b = PROJ_2(uId)
> IMPLIES
> integer_pred(((((PROJ_1(uId) + PROJ_2(uId)))
> *
> (((PROJ_2(uId)
> - PROJ_1(uId))
> + 1)))
> / 2)));
Put simply, the rhs of the implication is (where x and y are int):
integer_pred( (x*y) / 2)
The non-linear nature of this expression means the decision procedures
cannot automatically decide it. To prove it, start by assuming
that (x*y) is even, which should discharge the above. To discharge
the assumption, proceed by case analysis on the oddness/evenness of
x and y.
Dave
---
Dr Dave Stringer-Calvert, Software Engineer, Computer Science Laboratory,
SRI International, 333 Ravenswood Avenue, Menlo Park, CA 94025-3493, USA.
Phone: (650) 859-3291 Fax: (650) 859-2844 Email: dave_sc@csl.sri.com