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

PVS Bug 1065


Synopsis:        Typechecker Bug
Severity:        serious
Priority:        medium
Responsible:     owre
State:           open
Class:           sw-bug
Arrival-Date:    Wed Jul 28 09:30:00 -0700 2010
Originator:      "NARKAWICZ, ANTHONY JOSEPH. (LARC-D320)"
Release:         PVS 4.2
Organization:    nasa.gov
Environment: 
 System:          
 Architecture: 

Description: 
  --_003_D2852AE6C0FA2F40B650C08EF356AC75BCD968DE6FNDMSSCC05ndcn_
  Content-Type: text/plain; charset="us-ascii"
  Content-Transfer-Encoding: quoted-printable
  
  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_D2852AE6C0FA2F40B650C08EF356AC75BCD968DE6FNDMSSCC05ndcn_
  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_D2852AE6C0FA2F40B650C08EF356AC75BCD968DE6FNDMSSCC05ndcn_
  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_D2852AE6C0FA2F40B650C08EF356AC75BCD968DE6FNDMSSCC05ndcn_--

How-To-Repeat: 

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