Home Intro Announce FAQ Docs Download Mail Status Bugs Users Related FM Tools

PVS Bug 1005


Synopsis:        record modification
Severity:        serious
Priority:        medium
Responsible:     owre (Sam Owre)
State:           open
Class:           sw-bug
Arrival-Date:    Wed Sep 26 13:00:00 2007
Originator:      Hesselink
Organization:    rug.nl
Release:         PVS 4.0
Environment: 
 System:          
 Architecture: 

Description: 
  This is a multi-part message in MIME format.
  --------------080600070206020205030904
  Content-Type: text/plain; charset=ISO-8859-1; format=flowed
  Content-Transfer-Encoding: 7bit
  
  Dear Sam,
  
  It seems that modifying an element of a record and modifying an element 
  of an element of the same record do not combine. In the attached proof, 
  I would do tab E (apply extensionality), but that gives a lisp error.
  
  Best regards,
  Wim
  
  -- 
                          Wim H. Hesselink  
  
   Dept. of Computing Science       /   phone +31 50 3633933
      University of Groningen      /       or +31 50 3633939
                  P.O.Box 407     /     fax   +31 50 3633800
            9700 AK Groningen    /      email: w.h.hesselink@rug.nl
              The Netherlands   /       http://www.cs.rug.nl/~wim
  
  
  --------------080600070206020205030904
  Content-Type: text/plain;
   name="recordErrorDump"
  Content-Transfer-Encoding: 7bit
  Content-Disposition: inline;
   filename="recordErrorDump"
  
  
  %% PVS Version 4.0 - Allegro CL Enterprise Edition 8.0 [Mac OS X (Intel)] (No
 v 28, 2006 15:57)
  %% 8.0 [Mac OS X (Intel)] (Nov 28, 2006 15:57)
  $$$err.pvs
  err: THEORY
  BEGIN
    nP: posnat
    Process: TYPE = below(nP)
  
    Space: TYPE = [# 
      pc: [Process -> nat]
    #]
  
    add1(x: nat): nat = x+1
  
    x, y: VAR Space
    p: VAR Process
  
    pq(x): Space =
      x WITH [`pc := add1 o x`pc ]
  
    rs(p , x): Space =
      x WITH [`pc(p) := x`pc(p) + 1 ]
  
    commutate: LEMMA
      pq(rs(p, x)) = rs(p, pq(x))
  
  END err
      
  
  --------------080600070206020205030904--

How-To-Repeat: 

Fix: 
Home Intro Announce FAQ Docs Download Mail Status Bugs Users Related FM Tools