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

PVS Bug 869


Synopsis:        TCC bug probably not a TCC bug
Severity:        serious
Priority:        medium
Responsible:     owre (Sam Owre)
State:           analyzed
Class:           sw-bug
Arrival-Date:    Fri Nov 19 12:40:01 2004
Originator:      Pertti Kellomaki
Organization:    cs.tut.fi
Release:         PVS 3.2
Environment: 
 System:          
 Architecture: 

Description: 
  
  --Apple-Mail-3-183150651
  Content-Transfer-Encoding: 7bit
  Content-Type: text/plain;
  	charset=US-ASCII;
  	format=flowed
  
  Hi,
  
  I reported earlier today a bug in TCC generation. Further
  investigation suggests that it is really a bug involving beta
  reduction and function update. Here's a theory where the
  bug manifests itself. The beta reduction step is the crucial
  one.
  -- 
  Pertti
  
  --Apple-Mail-3-183150651
  Content-Transfer-Encoding: 7bit
  Content-Type: application/octet-stream;
  	x-unix-mode=0644;
  	name="bug.dump"
  Content-Disposition: attachment;
  	filename=bug.dump
  
  
  %% PVS Version 3.2
  %% 6.2 [Linux (x86)] (Nov 3, 2004 23:30)
  $$$PVSHOME/.pvs.lisp
  ; empty
  
  $$$PVSHOME/.pvs.lisp
  ; empty
  
  $$$bug.pvs
  bug2 : THEORY
  BEGIN
  
    T1 : DATATYPE BEGIN
      Nothing : Nothing?
      Something : Something?
    end T1
  
    T2 : TYPE = [nat -> T1]
  
    P(t : T2) : bool =
      forall (b : below(2)) :
        Something?(t(b))  =>
          every((lambda (a : nat) : false), (: 0 :))
  
    t2 : T2 =
           (lambda (addr : nat) : Nothing) WITH [
              (0) := Something, (1) := Something
             ]
    
    wf1 : THEOREM P(t2) and not P(t2)
  
    END bug2
  
  $$$bug.prf
  (bug2
   (P_TCC1 0
    (P_TCC1-1 nil 3309884241 nil ("" (subtype-tcc) nil nil) unfinished
     nil nil nil nil nil))
   (wf1 0
    (wf1-2 nil 3309884514 3309884529
     ("" (expand "t2")
      (("" (expand "P")
        (("" (prop)
          (("1" (beta) (("1" (skosimp*) nil nil)) nil)
           ("2" (inst -1 "0")
            (("2" (beta)
              (("2" (ground)
                (("2" (expand "every") (("2" (propax) nil nil)) nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil)
     proved
     ((t2 const-decl "T2" bug2 nil)
      (every adt-def-decl "boolean" list_adt nil)
      (below type-eq-decl nil naturalnumbers 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_field -> boolean]" reals nil)
      (number_field nonempty-type-from-decl nil number_fields nil)
      (number_field_pred const-decl "[number -> boolean]" number_fields
       nil)
      (boolean nonempty-type-decl nil booleans nil)
      (number nonempty-type-decl nil numbers nil)
      (P const-decl "bool" bug2 nil))
     12724 130 nil nil)
    (wf1-1 nil 3309881369 3309884499
     ("" (expand "bbi1")
      (("" (expand "P")
        (("" (prop)
          (("1" (beta) (("1" (skosimp*) nil nil)) nil)
           ("2" (inst -1 "0")
            (("2" (beta)
              (("2" (ground)
                (("2" (expand "every") (("2" (propax) nil nil)) nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil)
     unfinished
     ((P const-decl "bool" bug2 nil)
      (number nonempty-type-decl nil numbers nil)
      (boolean nonempty-type-decl nil booleans nil)
      (number_field_pred const-decl "[number -> boolean]" number_fields
       nil)
      (number_field nonempty-type-from-decl nil number_fields nil)
      (real_pred const-decl "[number_field -> 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)
      (< const-decl "bool" reals nil)
      (below type-eq-decl nil naturalnumbers nil) nil nil)
     27069 320 t shostak)))
  
  
  --Apple-Mail-3-183150651--

How-To-Repeat: 

Fix: 
Fixed find-update-commontype* (type-expr) to use judgement-types+ rather
than judgement-types

(defmethod find-update-commontype* ((te type-expr) expr (args null) value)
  (declare (ignore expr))
  (let ((tvalue (typecheck* (copy-untyped value) te nil nil)))
    (assert (and tvalue (type tvalue)))
    (reduce #'compatible-type (cons te (judgement-types+ tvalue)))))
Home Intro Announce FAQ Docs Download Mail Status Bugs Users Related FM Tools