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

problem




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