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

Re: [PVS-Help] Help with (both-sides) strategy



Hi Sam,

Here are my files:

Attachment: SelectorAssignment.pvs
Description: Binary data

Attachment: SelectorAssignment.prf
Description: Binary data


It’s with noting that p_Data_Type_Conversion is of type posint8_from_1_to_5, which is defined as:
posint8_from_1_to_5?(n: number): bool = posint8?(n) AND
  (1 <= n) AND (n <= 5);
posint8_from_1_to_5: NONEMPTY_TYPE = (posint8_from_1_to_5?)
  CONTAINING 1;

Cesar Muñoz has pointed out that if I replace “number” with “real” in my definition, my problem goes away. I still think the FALSE = TRUE issue seems problematic, but by switching all of my definitions of types from using numbers to using reals, I’ve reduced the generated TCCs by more than 20%, so that’s definitely something.

Best Regards,
Ben Hocking
ben.hocking@xxxxxxxxxxxxxxxxxxxxxxx

> On May 25, 2016, at 3:12 AM, Sam Owre <owre@xxxxxxxxxxx> wrote:
> 
> Hi Ben,
> 
> I'm having trouble recreating this.  With the spec
> 
> -----
> test: THEORY
> BEGIN
> p_Data_Type_Conversion: nat
> f: formula 1 <= p_Data_Type_Conversion => p_Data_Type_Conversion - 1 >= 0
> END test
> -----
> 
> I get:
> 
> f :  
> 
>  |-------
> {1}   1 <= p_Data_Type_Conversion IMPLIES p_Data_Type_Conversion - 1 >= 0
> 
> Rule? (flatten)
> Applying disjunctive simplification to flatten sequent,
> this simplifies to: 
> f :  
> 
> {-1}  1 <= p_Data_Type_Conversion
>  |-------
> {1}   p_Data_Type_Conversion - 1 >= 0
> 
> Rule? (both-sides "+" "1" 1)
> Applying + 1 to both sides of an inequality/equality conjunction,
> this simplifies to: 
> f :  
> 
> [-1]  1 <= p_Data_Type_Conversion
>  |-------
> {1}   p_Data_Type_Conversion - 1 + 1 >= 0 + 1
> 
> Rule?
> 
> I suspect that the decision procedures have already recorded something in
> your case that is affecting the behavior of both-sides (yours shows that
> you're in the fourth branch of the proof).  Is it possible for you to send
> me your specs?
> 
> Thanks,
> Sam
> 
> Ben Hocking <ben.hocking@xxxxxxxxxxxxxxxxxxxxxxx> wrote:
> 
>> From: Ben Hocking <ben.hocking@xxxxxxxxxxxxxxxxxxxxxxx>
>> Date: Mon, 23 May 2016 11:54:20 -0400
>> To: pvs-help@xxxxxxxxxxx
>> Subject: [PVS-Help] Help with (both-sides) strategy
>> Sender: pvs-help-bounces+owre=csl.sri.com@xxxxxxxxxxx
>> 
>> I don’t use the (both-sides) strategy very often, so perhaps I’m using it wrong, but I’m not sure what I’m doing
>> wrong in the following:
>> Selector_TCC2.4 :
>> 
>> [-1] (1 <= p_Data_Type_Conversion)
>> |-------
>> [1] p_Data_Type_Conversion - 1 >= 0
>> 
>> Rule? (both-sides "+" "1" 1)
>> Applying + 1 to both sides of an inequality/equality conjunction,
>> this yields 3 subgoals:
>> Selector_TCC2.4.1 :
>> 
>> [-1] (1 <= p_Data_Type_Conversion)
>> |-------
>> {1} p_Data_Type_Conversion - 1 + 1 >= 0 + 1
>> 
>> Rule? (grind)
>> Trying repeated skolemization, instantiation, and if-lifting,
>> 
>> This completes the proof of Selector_TCC2.4.1.
>> 
>> Selector_TCC2.4.2 :
>> 
>> [-1] (1 <= p_Data_Type_Conversion)
>> |-------
>> {1} p_Data_Type_Conversion - 1 >= 0 =
>> p_Data_Type_Conversion - 1 + 1 >= 0 + 1
>> [2] p_Data_Type_Conversion - 1 >= 0
>> 
>> Rule? (assert)
>> Simplifying, rewriting, and recording with decision procedures,
>> this simplifies to:
>> Selector_TCC2.4.2 :
>> 
>> [-1] (1 <= p_Data_Type_Conversion)
>> |-------
>> {1} FALSE = TRUE
>> [2] p_Data_Type_Conversion - 1 >= 0
>> 
>> At this point, since {1} is clearly false, I’m back to where I started (notwithstanding an additional TCC to prove
>> that real_pred(p_Data_Type_Conversion - 1), which can be proved with (lemma "reals.closed_minus" ("x"
>> "p_Data_Type_Conversion" "y" "1"))).
>> 
>> Any idea what I’m doing wrong?
>> 
>> And how does:
>> {1} p_Data_Type_Conversion - 1 >= 0 =
>> p_Data_Type_Conversion - 1 + 1 >= 0 + 1
>> get resolved to:
>> {1} FALSE = TRUE
>> upon using (assert)?
>> 
>> Best Regards,
>> Ben Hocking
>> ben.hocking@xxxxxxxxxxxxxxxxxxxxxxx
>