[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[PVS-Help] generic method, typecheck



Hello:
what's the meaning of PVS error message "No primary method for the
generic function" when typecheck a pvs theory

.................

bound_order: TYPE = {<, <=}

element: TYPE = [# cij: bound, lte: bound_order #]

PreDBM: TYPE = [upto(N), upto(N) -> element]

i, j , l: VAR upto(N)

DBM: TYPE =
{dbm: PreDBM |
FORALL i:
dbm(i, i) = zero AND
zero >= dbm(0, i) AND dbm(i, 0) >= zero}


gen(c: int, lte: bound_order):element = (#cij := finite(c), lte:=lte #)

gen(f: clkp): RECURSIVE DBM =
CASES f
OF <=(x, c):
LAMBDA i, j:
IF i = x AND j /= x THEN (# cij := finite(c), lte:=<= #) ELSE TRUE(i, j)
ENDIF,
>=(x, c): TRUE WITH [(0, x) := gen(-c, <=)],
<(x, c):
LAMBDA i, j:
IF i = x AND j /= x THEN gen(c, <) ELSE TRUE(i, j) ENDIF,
>(x, c): TRUE WITH [(0, x) := gen(-c, <)],
=(x, c):
LAMBDA i, j:
IF i = x AND j /= x THEN gen(c, <=)
ELSIF i = 0 AND j = x THEN gen(-c, <=)
ELSE TRUE(i, j)
ENDIF,
TRUE: TRUE,
AND(f1, f2): gen(f1) /\ gen(f2)
ENDCASES
MEASURE id BY <<
.................

when typecheck it give me an error message:

second argument to gen has the wrong type
Found: [[reals.real, reals.real] -> booleans.bool]
[[ordstruct_adt.ordstruct, ordstruct_adt.ordstruct] ->
booleans.bool]
[[defined_types[T].pred, defined_types[T].pred] ->
booleans.bool]
[[bound_domain.bound, bound_domain.bound] -> booleans.bool]
[[x: clkinterp[N].clock, clkp[N].clk_le_ub(x)] -> (clkp[N].le?)]
Expected: bound_order

why the pvs context cannot identify the <= is and data element of
bound_order


but if we change the recursive function's type as PredDBM , why the
typecheck success(without give me error message)?

who can help me?



thanks in advance!

Q.G. XU 07/02