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

PVS Bug 467


Synopsis:        Parse error while showing TCCs
Severity:        serious
Priority:        medium
Responsible:     owre
State:           analyzed
Class:           sw-bug
Arrival-Date:    Tue Jun 27 15:40:03 2000
Originator:      Sam Owre
Organization:    csl.sri.com
Release:         PVS 2.3
Environment: 
 System:          
 Architecture: 

Description: 
  While showing TCCs for a number judgement of the form, e.g.,
  
  JUDGEMENT 185 HAS_TYPE below[n]
  
  PVS generates a parse error.

How-To-Repeat: 

Fix: 

TCCs generated for number-judgements without ids are based on the number
itself.  Thus
  JUDGEMENT 13 HAS_TYPE (prime?)
generates the TCC
  thirteen_TCC1: prime?(13)
This is done using the ~R format directive from Common Lisp.

When the number gets large, e.g., 185, then ~R generates a number with
spaces and/or hyphens; in this case |one hundred eighty-five_TCC1|. This
is not legal PVS.  The fix is to modify the ref-to-id (number-judgement)
method to substitute underscores for spaces and hyphens in the generated
id.

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