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

PVS Bug 501


Synopsis:        failure in resolving constructor names
Severity:        serious
Priority:        medium
Responsible:     dave_sc (Dave Stringer-Calvert)
State:           analyzed
Class:           sw-bug
Arrival-Date:    Fri Dec 22 16:40:01 2000
Originator:      Joachim van den Berg
Organization:    cicero.cs.kun.nl
Release:         PVS 2.3
Environment: 
 System:          
 Architecture: 

Description: 
  Dear Sam, Dave,
  
  PVS has a problem with resolving constructors names. Below, I have included
  an example in which the problem occurs. Surprisingly enough, if I change
  abbrev[bool] in the IMPORTING of Test into e.g. abbrev[bool], or 
  abbrev[ADT[real]], then there is no problem at all.
  
  It would be great if this problem can be solved.
  
  Another remark: I noticed that there no judgements present for deciding
  that the type of a character is below(256). Perhaps these judgements should
  still be added to PVS, eg the judgement for "A":
  A_char : JUDGEMENT 65 HAS_TYPE below(256)
  
  Finally, I wish you a merry Christmas and a happy 2001!!!
  
  Best,
  Joachim van den Berg
  
  
  P.S. 
  I'm using PVS Version 2.3 (patch level 1.2.2.120) 
  Allegro CL Professional Edition 5.0 [Linux/X86] (9/4/99 13:27)
  running on RedHat Linux 6.2
  
  --
  
  
  ADT[T : TYPE] : DATATYPE
  BEGIN
    a : a?
    b (c : T) : b?
  END ADT
  
  
  abbrev[T : TYPE] : THEORY
  BEGIN
    IMPORTING ADT[T]
  
    adt? : TYPE = ADT[T]
  
  END abbrev
  
  Test[U : TYPE] : THEORY
  BEGIN
  
    IMPORTING abbrev[int], abbrev[real]
  
    x : VAR adt?[int]
  
    test : LEMMA
      CASES x OF
        a : TRUE,
        b(c) : TRUE
      ENDCASES
  
  END Test
  
  

How-To-Repeat: 

Fix: 

 [davesc]
 Fixed in 2.3.1.  Suggestion to be addressed.

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