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

PVS Bug 569

Synopsis:        Syntax incompatibility
Severity:        serious
Priority:        medium
Responsible:     owre
State:           analyzed
Class:           sw-bug
Arrival-Date:    Mon May 21 12:40:01 2001
Originator:      Paul Loewenstein
Organization:    lara.eng.sun.com
Release:         PVS 2.3

  		    PVS Version 2.3 (patch level
  The theory TCC_Syntax, below, fails to parse.  Of course, I could fix
  it so that it does, but unfortunately PVS' show-tccs sometimes uses
  the failing syntax (the [nat] (theory parameter) attached to the
  Absent and Present), which causes the show-tccs command to fail.
  By the way, for your information, I'm using PVS to verify (as much as
  I can) cache coherence protocols.  I can talk some more, but I can't
  divulge much about the protocols themselves.
  %   Description    :  A small theory of presence and absence
  bind  [ t: TYPE ]: THEORY
    bound: DATATYPE
      Absent: Absent?
      Present (Contents: t): Present?
    END bound
    bind_extensionality: THEOREM
      FORALL (x, y: t):  Present (x) = Present (y) IMPLIES x = y
    Present_1_1: THEOREM
      FORALL (x, y: t):  Present (x) = Present (y) IFF x = y
    Present_Contents_Lemma: LEMMA
      FORALL (x: (Present?), y: t): (Contents (x) = y) IMPLIES (x = Present (y)
    Contents_Present_Lemma: LEMMA
      FORALL (x: bound, y: t): (x = Present (y)) IFF (Present? (x) AND (Content
 s (x) = y))
    END bind
  TCC_Syntax: THEORY
      IMPORTING bind [nat]
      Test (x: bound [nat]): nat =
        CASES x OF
  	Absent[nat]:		0,
  	Present[nat] (y):	1 + y
    END TCC_Syntax


The spec isn't meant to parse; the bug is in the way the TCCs are
generated.  The fix is to just print the constructor id rather than
the full name:

(defmethod pp* ((sel selection))
  (with-slots (constructor args expression) sel
    (pprint-logical-block (nil nil)
      (pprint-indent :current 2)
      (write (id constructor))
      (when args
	(pprint-logical-block (nil args :prefix "(" :suffix ")")
	  (loop (write (id (pprint-pop)))
		(write-char #\,)
		(write-char #\space)
		(pprint-newline :fill))))
      (write-char #\:)
      (write-char #\space)
      (pprint-newline :fill)
      (pp* expression))))

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