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

Re: FW: PVS Problems

Hi Galina,

> I have two problems using the PVS, version 2.3, patch level

> 1) After proving the generated TCCs and the theorem (att. B029.pvs), I can
> not view the TCCs i.e. if I the click on the "Viewing TCCs" and then on
> "show-tccs", the content is empty and there is a message "parser error".
> Take into account, please, that during the process of proving the TCCS or
> the theorem, no error message appears.  

> As we don't have pvs e-mail working, I attached here the pvs files B029.pvs
> and math_fun.pvs. The math_fun.pvs has to be typechecked (and so
> math_fun.bin to be created) before running the B029.pvs.

> The problem can be avoided if in the function: 
> AbstG_AbstA2D_HTPressure(
>    x: ARRAY[subrange(1,4) -> subrange(0,5119)]): t_SnrValAll =
>    LAMBDA(i:subrange(1,48)):
>       COND
>          ((39 <= i) & (i <= 42))
>       -> AbstA2D(x((i - (39 - 1)))),
>          ELSE
>       -> epsilon(LAMBDA(randomVal:t_SnrValue): FALSE)
>       ENDCOND

> the ELSE is replaced by NOT((39 <= i) & (i <= 42)).

This problem has been fixed in the recently released PVS version 2.4.
Please download it from the PVS home page.  Your specification
implicitly uses the K_conversion, which is now off by default, so
you'll need to add the line
 CONVERSION K_conversion 
near the beginning of your spec.

Unfortunately your spec exposes a bug in PVS 2.4, so you'll also need
to load the following code (add it to your ~/.pvs.lisp file).

(defmethod application-conversion-argument (arg (conv name-expr) vars)
  (let ((var1 (find-if #'(lambda (v)
                           (tc-eq (type v) (domain (range (type conv)))))
    (if (some #'(lambda (ty)
                  (and (funtype? (find-supertype ty))
                       (compatible? (domain (find-supertype ty)) (type var1))))
              (ptypes arg))
        (let ((ac (make-instance 'argument-conversion
                    'operator arg
                    'argument var1)))
          (typecheck* ac nil nil nil))

> 2) In the att. CIOB051.pvs, among the other input parameters there are
> mk_SGLLcondIn and mk_SGLLcondOut. 
> The mk_SGLLcondIn is declared as a constant mk_SGLLcondIn: t_SGLLcondRange =
> 2349, where t_SGLLcondRange is subrange(2349, 3239).
> The mk_SGLLcondOut is declared as a variable: mk_SGLLcondOut: VAR {x:
> t_SGLLcondRange | x < mk_SGLLcondIn}.
> These two inputs are used in the function f_LogNLowForSGLLconditioning: 

> f_LogNLowForSGLLConditioning(
>    mk_SGLLcondIn: t_SGLLcondRange, 
>    mk_SGLLcondOut: {x:t_SGLLcondRange | x < mk_SGLLcondIn},
>    m_LogN: subrange(0,5119),
>    f_LogNLowForSGLLConditioning_s1: bool): bool =
>       COND
>          (m_LogN >= mk_SGLLcondIn)
>       ->  FALSE ,
>          ((mk_SGLLcondIn > m_LogN) & (m_LogN > mk_SGLLcondOut))
>       -> f_LogNLowForSGLLConditioning_s1,
>          (mk_SGLLcondOut >= m_LogN)
>       ->  TRUE 
>       ENDCOND

> As you can see, if mk_SGLLcondIn = 2349, then mk_SGLLcondOut has to be <
> 2349 and as the data type of mk_SGLLcondOut is subrange(2349, 3239), there
> is no x which can satisfied this condition. 
> In the process of proving this theorem, all tccs are proved and the theorem
> is proved as well.

> It is not the case, if in the function f_LogNLowForSGLLConditioning, for the
> input parameter mk_SGLLcondOut, an explicit value for the input constant
> mk_SGLLcondIn = 2349 is used:
> .....
> f_LogNLowForSGLLConditioning(
>    mk_SGLLcondIn: t_SGLLcondRange, 
>    mk_SGLLcondOut: {x:t_SGLLcondRange | x < 2349},
>    m_LogN: subrange(0,5119),
>    f_LogNLowForSGLLConditioning_s1: bool): bool = ...

> Then a type check error "Subtype TCC for mk_SGLLcondOut simplifies to FALSE"
> appears. As these two versions of the theorem look identical to me, why a
> typecheck error should appear in one of the cases? Actually I would expect
> that the same typecheck error will appear in both cases, as there is no x of
> data type t_SGLLcondRange, which is  < 2349. 
> Attached to this e-mail is the pvs file CIOB051.pvs. It has to be run from
> the same directory where math_fun.bin is(math_fun.bin is automatically
> produced if math_fun.pvs is typechecked).

The issue here is one of empty types.  These make sense
mathematically, and are legal in PVS, as long as no constant is
declared to be of that type, i.e., as long as only variables range
over the type.  Parameters in a function definition are always
variables, so they cause no problem even if their type is empty, but
there is then the issue that one may be defining the empty function,
which is perfectly OK mathematically, but often not what was intended.

One way to ensure that a function has a nontrivial definition is to
demonstrate that its domain is nonempty.  This usually happens as a
side effect of application, unless the function is only ever applied
variables.  This is what is happening in your case:
f_LogNLowForSGLLConditioning is invoked in vb_B051_1 and vb_B051_2
with second argument mk_SGLLcondOut, which is declared as a variable.

If you are concerned that some of your function definitions might
inadvertently be empty, I suggest you augment each of these
definitions with a lemma that asserts their domain is nonempty.

Sam Owre