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

PVS Bug 1067


Synopsis:        FW: Typechecker Bug
Severity:        serious
Priority:        medium
Responsible:     owre
State:           open
Class:           sw-bug
Arrival-Date:    Tue Sep 28 10:35:00 -0700 2010
Originator:      "Butler, Ricky W. (LARC-D320)"
Release:         PVS 4.2
Organization:    nasa.gov
Environment: 
 System:          
 Architecture: 

Description: 
  --_003_4B5CE520FC139D4E8A620ACC1D8AFB7D192CECFAD9NDMSSCC08ndcn_
  Content-Type: text/plain; charset="us-ascii"
  Content-Transfer-Encoding: quoted-printable
  
  Sam,
      Here is another PVS bug that is a high priority for us to have fixed. =
  =20
  It may be centered around a clash between our fseqs theory (structures libr=
  ary) and the finite sequences in the prelude.  I wonder if it would be adva=
  ntageous to restructure the PVS prelude into layers, e.g. layer 0 =3D bare =
  essentials, layer 1 =3D basic functions and theories, layer 2 adds the rest=
   with the ability of the users to only have layer 0 or layer 1 or layer 2 v=
  ia some start-up option.
  
  Rick
  
  -----Original Message-----
  From: NARKAWICZ, ANTHONY JOSEPH. (LARC-D320)=20
  Sent: Tuesday, September 28, 2010 8:41 AM
  To: Butler, Ricky W. (LARC-D320)
  Subject: FW: Typechecker Bug
  
  Ricky,
  
  Here is the pvs bug email that you wanted me to forward to you.
  
  -Anthony
  
  
  
  I believe that we are encountering a bug in PVS. Here is the system info:
  
  PVS Version: 4.2
  Emacs Version: 22.3.1
  OS: Darwin Kernel Version 10.4.0
  
  Bug Description: Two files are attached to this message, integral_def.pvs a=
  nd integral_prep.pvs. Each of these has a type [T: TYPE from real] as a the=
  ory parameter, and the theory integral_prep imports integral_def. The theor=
  y integral_def imports structures@fseqs[T] from the NASA libraries. The the=
  ory integral_def defines a new type abcd and typechecks perfectly well. How=
  ever, the theory integral_prep, which has a lemma that the type abcd[T] is =
  not empty, does not typecheck. The typechecker gets stuck on the type abcd[=
  T] and says "Could not determine the full theory instance". However, if the=
   [T: TYPE form real] theory parameter in each theory is replaced with [T:TY=
  PE], both files typecheck. That is, adding the "from real" in both cases ca=
  uses the typechecker to fail in integral_prep.
  
  
  
  Thanks,
  
  Anthony Narkawicz
  
  --_003_4B5CE520FC139D4E8A620ACC1D8AFB7D192CECFAD9NDMSSCC08ndcn_
  Content-Type: application/octet-stream; name="integral_def.pvs"
  Content-Description: integral_def.pvs
  Content-Disposition: attachment; filename="integral_def.pvs"; size=145;
  	creation-date="Wed, 28 Jul 2010 11:01:56 GMT";
  	modification-date="Wed, 28 Jul 2010 11:01:56 GMT"
  Content-Transfer-Encoding: base64
  
  aW50ZWdyYWxfZGVmW1Q6IFRZUEUgZnJvbSByZWFsXTogVEhFT1JZCgpCRUdJTgoKCiAgIElNUE9S
  VElORyBzdHJ1Y3R1cmVzQGZzZXFzW1RdCgoKICAgYWJjZDogVFlQRSA9IGZzZXFbVF0KCiAgICAg
  ICAgICAgICAgIAoKCkVORCBpbnRlZ3JhbF9kZWYKCg==
  
  --_003_4B5CE520FC139D4E8A620ACC1D8AFB7D192CECFAD9NDMSSCC08ndcn_
  Content-Type: application/octet-stream; name="integral_prep.pvs"
  Content-Description: integral_prep.pvs
  Content-Disposition: attachment; filename="integral_prep.pvs"; size=147;
  	creation-date="Wed, 28 Jul 2010 11:02:04 GMT";
  	modification-date="Wed, 28 Jul 2010 11:02:04 GMT"
  Content-Transfer-Encoding: base64
  
  aW50ZWdyYWxfcHJlcFtUOiBUWVBFIGZyb20gcmVhbF06IFRIRU9SWQoKQkVHSU4KCgogICBJTVBP
  UlRJTkcgaW50ZWdyYWxfZGVmW1RdCgoKICAgZm9vOiBMRU1NQSBFWElTVFMgKFA6IGFiY2RbVF0p
  OiBUUlVFCgoKCkVORCBpbnRlZ3JhbF9wcmVwCgoKCgoK
  
  --_003_4B5CE520FC139D4E8A620ACC1D8AFB7D192CECFAD9NDMSSCC08ndcn_--

How-To-Repeat: 

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