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

PVS Bug 709


Synopsis:        Minor bugs in PVS3
Severity:        serious
Priority:        medium
Responsible:     dave_sc (Dave Stringer-Calvert)
State:           analyzed
Class:           sw-bug
Arrival-Date:    Thu Aug 15 15:40:01 2002
Originator:      Bruno Dutertre
Organization:    sdl.sri.com
Release:         PVS 2.4
Environment: 
 System:          
 Architecture: 

Description: 
  This is a multi-part message in MIME format.
  --------------070700030907080407000301
  Content-Type: text/plain; charset=us-ascii; format=flowed
  Content-Transfer-Encoding: 7bit
  
  Sam,
  
  Typechecking the same theory twice may give a different
  number of warnings or messages. I think this can be
  reproduced in the attached example by
  - typecheck "events"
  - force-typecheck "basics"
  - typecheck "events" again
  
  There will be twice the same warning:
  
  Warnings for theory events:
  
  Datatype event may be empty
  
  Datatype event may be empty
  
  
  
  The other problem is with proof scripts recovered
  from orphaned-proof.prf. If you do show-orphaned-proofs,
  then select a proof from there, you get a Proof script
  in the new proof format. Then if you try to attach this
  script to a formula (by C-c C-i), you get a PVS Error:
  
  Label must be a string of numbers.
  
  Bruno
  
  --------------070700030907080407000301
  Content-Type: text/plain;
   name="events.dmp"
  Content-Transfer-Encoding: 7bit
  Content-Disposition: inline;
   filename="events.dmp"
  
  
  $$$events.pvs
  events: THEORY
  
    BEGIN
  
    IMPORTING basics
  
    % Two event types:
    % - request(i, m): leader i receives a request for m
    % - support(i, j, m): leader j receives support for m from i
  
  
    event: DATATYPE
      BEGIN
        request(rcv: leader, msg: message): request?
        support(snd: leader, rcv: leader, msg: message): support?
      END event
  
    % Rewrite rules for automating proofs 
  
    m1, m2: VAR message
    i1, i2, j1, j2: VAR leader
  
    equal_supports: LEMMA
       support(i1, j1, m1) = support(i2, j2, m2) IFF i1=i2 AND j1=j2 AND m1=m2
  
    equal_requests: LEMMA
       request(i1, m1) = request(i2, m2) IFF i1=i2 AND m1=m2
  
    END events
  
  $$$events.prf
  (events
   (event_request_extensionality 0
    (event_request_extensionality-1 nil 3238355680 nil nil nil nil nil
     nil nil shostak))
   (event_request_eta 0
    (event_request_eta-1 nil 3238355680 nil nil nil nil nil nil nil
     shostak))
   (event_support_extensionality 0
    (event_support_extensionality-1 nil 3238422510 nil nil nil nil nil
     nil nil shostak))
   (event_support_eta 0
    (event_support_eta-1 nil 3238422510 nil nil nil nil nil nil nil
     shostak))
   (event_rcv_request 0
    (event_rcv_request-1 nil 3238422510 nil nil nil nil nil nil nil
     shostak))
   (event_msg_request 0
    (event_msg_request-1 nil 3238355680 nil nil nil nil nil nil nil
     shostak))
   (event_snd_support 0
    (event_snd_support-1 nil 3238422510 nil nil nil nil nil nil nil
     shostak))
   (event_rcv_support 0
    (event_rcv_support-1 nil 3238422510 nil nil nil nil nil nil nil
     shostak))
   (event_msg_support 0
    (event_msg_support-1 nil 3238422510 nil nil nil nil nil nil nil
     shostak))
   (event_inclusive 0
    (event_inclusive-1 nil 3238355680 nil nil nil nil nil nil nil
     shostak))
   (event_disjoint 0
    (event_disjoint-1 nil 3238355680 nil nil nil nil nil nil nil
     shostak))
   (event_induction 0
    (event_induction-1 nil 3238355680 nil nil nil nil nil nil nil
     shostak))
   (event_well_founded 0
    (event_well_founded-1 nil 3238355680 nil nil nil nil nil nil nil
     shostak))
   (equal_supports 0
    (equal_supports-2 nil 3238423752 3238423760
     ("" (reduce)
      (("1" (case "msg(support(i1!1, j1!1, m1!1)) = m2!1")
        (("1" (assert) nil nil)
         ("2" (replace*) (("2" (assert) nil nil)) nil))
        nil)
       ("2" (case "rcv(support(i1!1, j1!1, m1!1)) = j2!1")
        (("1" (assert) nil nil)
         ("2" (replace*) (("2" (assert) nil nil)) nil))
        nil)
       ("3" (case "snd(support(i1!1, j1!1, m1!1)) = i2!1")
        (("1" (assert) nil nil)
         ("2" (replace*) (("2" (assert) nil nil)) nil))
        nil))
      nil)
     proved
     ((leader nonempty-type-eq-decl nil basics nil)
      (n const-decl "posnat" basics nil)
      (posnat nonempty-type-eq-decl nil integers nil)
      (> const-decl "bool" reals nil)
      (nonneg_int nonempty-type-eq-decl nil integers nil)
      (nat nonempty-type-eq-decl nil naturalnumbers nil)
      (>= const-decl "bool" reals nil)
      (int nonempty-type-eq-decl nil integers nil)
      (integer_pred const-decl "[rational -> boolean]" integers nil)
      (rational nonempty-type-from-decl nil rationals nil)
      (rational_pred const-decl "[real -> boolean]" rationals nil)
      (< const-decl "bool" reals nil)
      (real nonempty-type-from-decl nil reals nil)
      (real_pred const-decl "[number -> boolean]" reals nil)
      (number nonempty-type-decl nil numbers nil)
      (NOT const-decl "[bool -> bool]" booleans nil)
      (bool nonempty-type-eq-decl nil booleans nil)
      (boolean nonempty-type-decl nil booleans nil)
      (message type-decl nil basics nil)
      (= const-decl "[T, T -> boolean]" equalities nil)
      (event type-decl nil events nil)
      (msg adt-accessor-decl "[event -> message]" events nil)
      (support? adt-recognizer-decl "[event -> boolean]" events nil)
      (support adt-constructor-decl
       "[[leader, leader, message] -> (support?)]" events nil)
      (rcv adt-accessor-decl "[event -> leader]" events nil)
      (snd adt-accessor-decl "[(support?) -> leader]" events nil))
     6015 790 t nil)
    (equal_supports-1 nil 3238423680 nil nil untried nil nil nil nil
     shostak))
   (equal_requests 0
    (equal_requests-2 nil 3238355867 3238422927
     ("" (reduce)
      (("1" (case "msg(request(i1!1, m1!1)) = m2!1")
        (("1" (assert) nil nil)
         ("2" (replace*) (("2" (assert) nil nil)) nil))
        nil)
       ("2" (case "rcv(request(i1!1, m1!1)) = i2!1")
        (("1" (assert) nil nil)
         ("2" (replace*) (("2" (assert) nil nil)) nil))
        nil))
      nil)
     unchecked
     ((rcv adt-accessor-decl "[event -> leader]" events nil)
      (request adt-constructor-decl "[[leader, message] -> (request?)]"
       events nil)
      (request? adt-recognizer-decl "[event -> boolean]" events nil)
      (msg adt-accessor-decl "[event -> message]" events nil)
      (event type-decl nil events nil)
      (= const-decl "[T, T -> boolean]" equalities nil)
      (message type-decl nil basics nil)
      (boolean nonempty-type-decl nil booleans nil)
      (bool nonempty-type-eq-decl nil booleans nil)
      (NOT const-decl "[bool -> bool]" booleans nil)
      (number nonempty-type-decl nil numbers nil)
      (real_pred const-decl "[number -> boolean]" reals nil)
      (real nonempty-type-from-decl nil reals nil)
      (< const-decl "bool" reals nil)
      (rational_pred const-decl "[real -> boolean]" rationals nil)
      (rational nonempty-type-from-decl nil rationals nil)
      (integer_pred const-decl "[rational -> boolean]" integers nil)
      (int nonempty-type-eq-decl nil integers nil)
      (>= const-decl "bool" reals nil)
      (nat nonempty-type-eq-decl nil naturalnumbers nil)
      (nonneg_int nonempty-type-eq-decl nil integers nil)
      (> const-decl "bool" reals nil)
      (posnat nonempty-type-eq-decl nil integers nil)
      (n const-decl "posnat" basics nil)
      (leader nonempty-type-eq-decl nil basics nil))
     53984 6250 t nil)))
  
  
  $$$basics.pvs
  basics : THEORY
  
    BEGIN
  
    IMPORTING finite_sets@finite_sets
  
    %---------------
    % message type
    %---------------
  
    message: TYPE
    
    %--------------------------------------------
    % Parameters: number of leaders and maximal
    % number of faults
    %--------------------------------------------
  
    n: posnat
  
    f: { x: nat | 3 * x < n }
  
    faulty_bound1: LEMMA n - f >= 2*f + 1
  
    faulty_bound2: LEMMA n - f >= f + 1
  
  
    %----------
    % leaders
    %----------
   
    leader: NONEMPTY_TYPE = below(n)
  
    finite_leaders: JUDGEMENT set[leader] SUBTYPE_OF finite_set[leader]
  
    % lemmas on the cardinality of sets of leaders
    % extension of finite_sets@finite_sets
  
    s, s1, s2: VAR set[leader]
  
    card_fullset: LEMMA card(fullset[leader]) = n
  
    card_complement: LEMMA card(complement(s)) = n - card(s)
  
    max_card: JUDGEMENT card(s) HAS_TYPE upto(n)
  
    END basics
  
  $$$basics.prf
  (basics
   (f_TCC1 0
    (f_TCC1-1 nil 3238355135 3238355175
     ("" (inst + "0") (("" (assert) nil nil)) nil) proved-complete
     ((n const-decl "posnat" basics nil)
      (posnat nonempty-type-eq-decl nil integers nil)
      (> const-decl "bool" reals nil)
      (nonneg_int nonempty-type-eq-decl nil integers nil)
      (* const-decl "[real, real -> real]" reals nil)
      (< const-decl "bool" reals nil)
      (nat nonempty-type-eq-decl nil naturalnumbers nil)
      (>= const-decl "bool" reals nil)
      (bool nonempty-type-eq-decl nil booleans nil)
      (int nonempty-type-eq-decl nil integers nil)
      (integer_pred const-decl "[rational -> boolean]" integers nil)
      (rational nonempty-type-from-decl nil rationals nil)
      (rational_pred const-decl "[real -> boolean]" rationals nil)
      (real nonempty-type-from-decl nil reals nil)
      (real_pred const-decl "[number -> boolean]" reals nil)
      (boolean nonempty-type-decl nil booleans nil)
      (number nonempty-type-decl nil numbers nil))
     9305 1450 t shostak))
   (faulty_bound1 0
    (faulty_bound1-1 nil 3238359533 3238422013
     ("" (case "3 * f <= n-1")
      (("1" (assert) nil nil)
       ("2" (typepred "f")
        (("2" (name-replace "fff" "3 * f") (("2" (assert) nil nil)) nil))
        nil))
      nil)
     unchecked
     ((NOT const-decl "[bool -> bool]" booleans nil)
      (= const-decl "[T, T -> boolean]" equalities nil)
      (number nonempty-type-decl nil numbers nil)
      (boolean nonempty-type-decl nil booleans nil)
      (real_pred const-decl "[number -> boolean]" reals nil)
      (real nonempty-type-from-decl nil reals nil)
      (bool nonempty-type-eq-decl nil booleans nil)
      (<= const-decl "bool" reals nil)
      (* const-decl "[real, real -> real]" reals nil)
      (rational_pred const-decl "[real -> boolean]" rationals nil)
      (rational nonempty-type-from-decl nil rationals nil)
      (integer_pred const-decl "[rational -> boolean]" integers nil)
      (int nonempty-type-eq-decl nil integers nil)
      (>= const-decl "bool" reals nil)
      (nat nonempty-type-eq-decl nil naturalnumbers nil)
      (< const-decl "bool" reals nil)
      (nonneg_int nonempty-type-eq-decl nil integers nil)
      (> const-decl "bool" reals nil)
      (posnat nonempty-type-eq-decl nil integers nil)
      (n const-decl "posnat" basics nil)
      (f const-decl "{x: nat | 3 * x < n}" basics nil)
      (- const-decl "[real, real -> real]" reals nil))
     1141 560 t shostak))
   (faulty_bound2 0
    (faulty_bound2-1 nil 3238359533 3238422014
     ("" (lemma "faulty_bound1") (("" (assert) nil nil)) nil) unchecked
     ((faulty_bound1 formula-decl nil basics nil)) 307 290 t shostak))
   (leader_TCC1 0
    (leader_TCC1-1 nil 3238422009 3238422089
     ("" (inst + "0") (("" (assert) nil nil)) nil) proved-complete
     ((n const-decl "posnat" basics nil)
      (posnat nonempty-type-eq-decl nil integers nil)
      (> const-decl "bool" reals nil)
      (nonneg_int nonempty-type-eq-decl nil integers nil)
      (< const-decl "bool" reals nil)
      (nat nonempty-type-eq-decl nil naturalnumbers nil)
      (>= const-decl "bool" reals nil)
      (bool nonempty-type-eq-decl nil booleans nil)
      (int nonempty-type-eq-decl nil integers nil)
      (integer_pred const-decl "[rational -> boolean]" integers nil)
      (rational nonempty-type-from-decl nil rationals nil)
      (rational_pred const-decl "[real -> boolean]" rationals nil)
      (real nonempty-type-from-decl nil reals nil)
      (real_pred const-decl "[number -> boolean]" reals nil)
      (boolean nonempty-type-decl nil booleans nil)
      (number nonempty-type-decl nil numbers nil))
     10448 1340 t shostak))
   (finite_leaders 0
    (finite_leaders-1 nil 3238422009 3238422314
     ("" (grind :if-match nil)
      (("" (inst + "n" "lambda (i: (x!1)): i") (("" (assert) nil nil))
        nil))
      nil)
     proved-complete
     ((number nonempty-type-decl nil numbers nil)
      (boolean nonempty-type-decl nil booleans nil)
      (real_pred const-decl "[number -> boolean]" reals nil)
      (real nonempty-type-from-decl nil reals nil)
      (rational_pred const-decl "[real -> boolean]" rationals nil)
      (rational nonempty-type-from-decl nil rationals nil)
      (integer_pred const-decl "[rational -> boolean]" integers nil)
      (int nonempty-type-eq-decl nil integers nil)
      (bool nonempty-type-eq-decl nil booleans nil)
      (>= const-decl "bool" reals nil)
      (nat nonempty-type-eq-decl nil naturalnumbers nil)
      (nonneg_int nonempty-type-eq-decl nil integers nil)
      (> const-decl "bool" reals nil)
      (posnat nonempty-type-eq-decl nil integers nil)
      (n const-decl "posnat" basics nil) (< const-decl "bool" reals nil)
      (leader nonempty-type-eq-decl nil basics nil)
      (set type-eq-decl nil sets nil)
      (below type-eq-decl nil nat_types nil)
      (is_finite const-decl "bool" finite_sets_def nil)
      (injective? const-decl "bool" functions nil))
     42627 2210 t shostak))
   (card_fullset 0
    (card_fullset-1 nil 3238434200 3238434261
     ("" (rewrite "card_bij")
      (("" (inst + "lambda (i: (fullset[leader])): i")
        (("" (grind) nil nil)) nil))
      nil)
     unchecked
     ((below type-eq-decl nil nat_types nil)
      (bijective? const-decl "bool" functions nil)
      (surjective? const-decl "bool" functions nil)
      (injective? const-decl "bool" functions nil)
      (leader nonempty-type-eq-decl nil basics nil)
      (n const-decl "posnat" basics nil)
      (posnat nonempty-type-eq-decl nil integers nil)
      (> const-decl "bool" reals nil)
      (nonneg_int nonempty-type-eq-decl nil integers nil)
      (< const-decl "bool" reals nil)
      (nat nonempty-type-eq-decl nil naturalnumbers nil)
      (>= const-decl "bool" reals nil)
      (bool nonempty-type-eq-decl nil booleans nil)
      (int nonempty-type-eq-decl nil integers nil)
      (integer_pred const-decl "[rational -> boolean]" integers nil)
      (rational nonempty-type-from-decl nil rationals nil)
      (rational_pred const-decl "[real -> boolean]" rationals nil)
      (real nonempty-type-from-decl nil reals nil)
      (real_pred const-decl "[number -> boolean]" reals nil)
      (boolean nonempty-type-decl nil booleans nil)
      (number nonempty-type-decl nil numbers nil)
      (fullset const-decl "set" sets nil)
      (finite_set type-eq-decl nil finite_sets_def nil)
      (is_finite const-decl "bool" finite_sets_def nil)
      (set type-eq-decl nil sets nil)
      (card_bij formula-decl nil finite_sets "finite_sets/"))
     58070 4360 t shostak))
   (card_complement 0
    (card_complement-1 nil 3238434200 3238434452
     ("" (skolem!)
      ((""
        (auto-rewrite "card_fullset" "card_diff_subset" "subset_fullset")
        (("" (rewrite "difference_fullset2" :dir rl)
          (("" (assert) nil nil)) nil))
        nil))
      nil)
     unchecked
     ((subset_fullset formula-decl nil sets_lemmas nil)
      (card_fullset formula-decl nil basics nil)
      (card_diff_subset formula-decl nil finite_sets "finite_sets/")
      (leader nonempty-type-eq-decl nil basics nil)
      (n const-decl "posnat" basics nil)
      (posnat nonempty-type-eq-decl nil integers nil)
      (> const-decl "bool" reals nil)
      (nonneg_int nonempty-type-eq-decl nil integers nil)
      (< const-decl "bool" reals nil)
      (nat nonempty-type-eq-decl nil naturalnumbers nil)
      (>= const-decl "bool" reals nil)
      (bool nonempty-type-eq-decl nil booleans nil)
      (int nonempty-type-eq-decl nil integers nil)
      (integer_pred const-decl "[rational -> boolean]" integers nil)
      (rational nonempty-type-from-decl nil rationals nil)
      (rational_pred const-decl "[real -> boolean]" rationals nil)
      (real nonempty-type-from-decl nil reals nil)
      (real_pred const-decl "[number -> boolean]" reals nil)
      (boolean nonempty-type-decl nil booleans nil)
      (number nonempty-type-decl nil numbers nil)
      (set type-eq-decl nil sets nil)
      (difference_fullset2 formula-decl nil sets_lemmas nil))
     155633 3100 t shostak))
   (max_card 0
    (max_card-1 nil 3238434572 3238434611
     ("" (skolem!)
      (("" (rewrite "card_fullset" :dir rl)
        (("" (rewrite "card_subset")
          (("" (rewrite "subset_fullset") nil nil)) nil))
        nil))
      nil)
     proved
     ((card_fullset formula-decl nil basics nil)
      (subset_fullset formula-decl nil sets_lemmas nil)
      (leader nonempty-type-eq-decl nil basics nil)
      (n const-decl "posnat" basics nil)
      (posnat nonempty-type-eq-decl nil integers nil)
      (> const-decl "bool" reals nil)
      (nonneg_int nonempty-type-eq-decl nil integers nil)
      (< const-decl "bool" reals nil)
      (nat nonempty-type-eq-decl nil naturalnumbers nil)
      (>= const-decl "bool" reals nil)
      (bool nonempty-type-eq-decl nil booleans nil)
      (int nonempty-type-eq-decl nil integers nil)
      (integer_pred const-decl "[rational -> boolean]" integers nil)
      (rational nonempty-type-from-decl nil rationals nil)
      (rational_pred const-decl "[real -> boolean]" rationals nil)
      (real nonempty-type-from-decl nil reals nil)
      (real_pred const-decl "[number -> boolean]" reals nil)
      (boolean nonempty-type-decl nil booleans nil)
      (number nonempty-type-decl nil numbers nil)
      (fullset const-decl "set" sets nil)
      (finite_set type-eq-decl nil finite_sets_def nil)
      (is_finite const-decl "bool" finite_sets_def nil)
      (set type-eq-decl nil sets nil)
      (card_subset formula-decl nil finite_sets "finite_sets/"))
     30682 2890 t shostak)))
  
  
  --------------070700030907080407000301--
  

How-To-Repeat: 

Fix: 
Fixed pvs-select-proof and untypecheck.lisp.
Home Intro Announce FAQ Docs Download Mail Status Bugs Users Related FM Tools