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

*To*: pvs-help@csl.sri.com*Subject*: problem*From*: Jason Wu <wuhong@mcserg.cas.mcmaster.ca>*Date*: Mon, 23 Oct 2000 21:34:03 -0400 (EDT)*Delivery-Date*: Mon Oct 23 18:31:50 2000

Dear experts: I met the following problem while trying to prove a theorem involving the recursive function c_sealed_in () using type t as one of its arguments. (1) I define t as a non-negative real number as follows *** type declaration ******************** K: posreal non_neg: TYPE = { x: real | x>=0 } CONTAINING 0 time: TYPE = non_neg t: VAR time clock: TYPE = { t: time | EXISTS(n: nat): t=n*K } CONTAINING 0 x: VAR clock init(x): bool = (x=0) noninit_elem: TYPE ={ x | not init(x) } y: VAR noninit_elem pre(y): clock = y - K (2) I defined a recursive function using t as its arguments. ****** function definition c_sealed_in(param_trip,manual_reset)(t): RECURSIVE bool = IF init(t) THEN TRUE ELSE COND Held_For(param_trip,seal_in_delay)(t) -> TRUE, NOT Held_For(param_trip,seal_in_delay)(t) AND manual_reset(t) -> FALSE, NOT Held_For(param_trip,seal_in_delay)(t) AND NOT manual_reset(t) -> c_sealed_in(param_trip,manual_reset)(pre(t)), ENDCOND ENDIF MEASURE rank(t) (3) In the actual proof, we get the sequent Seal.1 as follows ****** problematic sequent ***************** Seal.1: {-1} (x!1 = 0) {-2} c_sealed_in(param_trip!1, manual_reset!1)(0) |------- {1} (4) After expanding the function definition, pre(0) appears as an argument to function c_sealed_in(). So we encounter infinite loop after using grind. Rule? (EXPAND "c_sealed_in") Expanding the definition of c_sealed_in, this simplifies to: Seal.1: [-1] (x!1 = 0) {-2} IF 0=0 THEN TRUE ELSE COND Held_For(param_trip!1, seal_in_delay)(0) -> TRUE, manual_reset!1(0) -> FALSE, ELSE -> c_sealed_in(param_trip!1, manual_reset!1)(pre(0)) ENDCOND ENDIF |------- [1] (5) My question: Since we define the argument t as a non-negative real number, why the PVS allows the negative number appear as the function argument after rewriting the recursive function? Is this a problem in my function definition or a PVS bug. Thanks for your insightful comments and help Jason

- Prev by Date:
**PVS Model-checker** - Next by Date:
**Data structure of real valued functions** - Prev by thread:
**Data structure of real valued functions (& PVS being too clever?)** - Next by thread:
**PVS Model-checker** - Index(es):