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

Re: assumptions/obligations



>  In chunnel.pvs I have, for instance, a theory 'points' which
> defines a type 'points_value' and an assumption on this type
> 'points_ax'. In the theory 'Thedford_scenario' a constant 'mp' of
> type 'points_value' is declared and instantiated. I thought that
> this would then incur an obligation to prove the assumption
> 'points_ax'. However, on doing a typecheck no such tcc occurs. Why
> is this? Is there any other way to write this so that the relevant
> tcc's occur?
> 
> Richard.

Assumptions require you to prove theorems on the formal parameters
passed into a theory.  That's not happening in your case.  This is
described in slightly more detail in the PVS language spec in section
6.

Here's a way to define point_values so it generates your desired tcc's
There's probably a slicker way to do it, but I think you'll get the
idea.

point_values: TYPE = ({(mpv : finseq[real] ) | 
          length(mpv) >= 2
              AND (FORALL (i: nat): member(i, {n: nat | n <= length(mpv) - 2}) IMPLIES seq(mpv)(i) > seq(mpv)(i + 1))})
    


cheers,

John


==============================++====================
John Hoffman, PhD             ||                    
Secure Computing Corporation  || What do you want to
2675 Long Lake Road           || read for, when you 
Roseville, MN  55113          || can watch TV?      
hoffman@securecomputing.com   ||                    
Fax  :(612)628-2701           ||  - Matilda's Father
Phone:(612)628-2808           ||                    
==============================++====================