[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