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

PVS Bug 663


Synopsis:        TCC generation bugs
Severity:        serious
Priority:        medium
Responsible:     owre
State:           analyzed
Class:           sw-bug
Arrival-Date:    Fri Mar 29 02:55:00 2002
Originator:      Chris George
Organization:    iist.unu.edu
Release:         PVS 2.4
Environment: 
 System:          
 Architecture: 

Description: 
  Both the theories below generate a parser error when show-tccs is used. 
  This is a feature of 2.4, not 2.3.
  
  The second can be cured by removing the brackets around the first formal
  parameter.
  
  bug: THEORY
  
  BEGIN
     f71: setof[[real, nat]] = {(y: real, x: nat) | x < 3 AND y > 0 }
  
     f711: setof[[real, nat]] = {(y: real, x: nat  | x = 1) | member((x,
  y), f71) }
  
  END bug
  
  complist [T:TYPE, U:TYPE]: THEORY
  BEGIN
  
  comp_list((l:list[T]), p:[T->bool], f:[T -> U]): RECURSIVE list[U] =
    CASES l of
      null: null,
      cons(h, t): 
        IF p(h) THEN cons(f(h), comp_list(t, p, f)) 
        ELSE comp_list(t, p, f) ENDIF
    ENDCASES
    MEASURE length(l)
  
  END complist
  

How-To-Repeat: 

Fix: 
TCCs are unparsed and parsed again in order to get the place set
correctly for the tccs buffer, but extraneous parens were added in this case.
Modified pp-paren-adformals* to better control the parenthesization.

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