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

FW: PVS Problems



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: 
   x: ARRAY[subrange(1,4) -> subrange(0,5119)]): t_SnrValAll =
         ((39 <= i) & (i <= 42))
      -> AbstA2D(x((i - (39 - 1)))),
      -> epsilon(LAMBDA(randomVal:t_SnrValue): FALSE)

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

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: 

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

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:
   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).

Best wishes: Galina Teneva