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

PVS Bug 1011


Synopsis:        Theory Interpretations (bug?)
Severity:        serious
Priority:        medium
Responsible:     owre (Sam Owre)
State:           open
Class:           sw-bug
Arrival-Date:    Mon Nov 12 14:55:00 2007
Originator:      "Cesar Munoz"
Organization:    nianet.org
Release:         PVS 4.1
Environment: 
 System:          
 Architecture: 

Description: 
  This is a multi-part message in MIME format.
  
  ------_=_NextPart_001_01C824BD.9AAA8246
  Content-Type: multipart/alternative;
  	boundary="----_=_NextPart_002_01C824BD.9AAA8246"
  
  
  ------_=_NextPart_002_01C824BD.9AAA8246
  Content-Type: text/plain;
  	charset="iso-8859-1"
  Content-Transfer-Encoding: quoted-printable
  
  
  Hi Sam,
  I'm preparing a lecture on Theory Interpretations for the PVS Class. Type=
  checking the following theory fails with the message: "Error: No methods ap=
  plicable for generic function". I wonder if I'm missing something, or if th=
  is is bug in PVS4.1 
  
  Thanks,
  Cesar
  
   
  
  
  
  
  
  
  
  
  
   National Institute of Aerospace: This e-mail message (including all atta=
  chments transmitted with it, if any) is intended solely for the use of the =
  addressee and may contain company proprietary information. If you are not t=
  he person to whom this e-mail is addressed, or an employee or agent respons=
  ible for delivering this message to the person to whom it is addressed, you=
   are hereby notified that any dissemination, distribution, copying, or othe=
  r use of this message or its attachments is strictly prohibited. If you hav=
  e received this e-mail in error, please notify the sender immediately by e-=
  mail reply, then please delete this e-mail, together with any attachments t=
  o it, from your computer. 
  ------_=_NextPart_002_01C824BD.9AAA8246
  Content-Type: text/html;
  	charset="iso-8859-1"
  Content-Transfer-Encoding: quoted-printable
  
  <!DOCTYPE HTML PUBLIC "-//W3C//DTD HTML 3.2//EN">
  <HTML>
  <HEAD>
  <META HTTP-EQUIV=3D"Content-Type" CONTENT=3D"text/html; charset=3Diso-885=
  9-1">
  <META NAME=3D"Generator" CONTENT=3D"MS Exchange Server version 6.5.7650.2=
  8">
  <TITLE>Theory Interpretations (bug?)</TITLE>
  </HEAD>
  <BODY><P>
  <!-- Converted from text/plain format -->
  <BR>
  
  <P><FONT SIZE=3D2>Hi Sam,<BR>
  I'm preparing a lecture on Theory Interpretations for the PVS Class. Type=
  checking the following theory fails with the message: &quot;Error: No metho=
  ds applicable for generic function&quot;. I wonder if I'm missing something=
  , or if this is bug in PVS4.1<BR>
  <BR>
  Thanks,<BR>
  Cesar<BR>
  </FONT>
  </P>
  
   </P>
  <P>
  <P>
  <HR style=3D"HEIGHT: 1px">
  
  <P></P>
  <P><FONT face=3DVerdana size=3D2><STRONG></STRONG></FONT></P>
  <P><FONT size=3D1><EM>&nbsp;National Institute of Aerospace: <FONT face=
  =3DArial>This 
  e-mail message (including all attachments transmitted with it, if any) is=
   
  intended solely for the use of the addressee and may contain company prop=
  rietary 
  information. If you are not the person to whom this e-mail is addressed, =
  or an 
  employee or agent responsible for delivering this message to the person t=
  o whom 
  it is addressed, you are hereby notified that any dissemination, distribu=
  tion, 
  copying, or other use of this message or its attachments is strictly proh=
  ibited. 
  If you have received this e-mail in error, please notify the sender immed=
  iately 
  by e-mail reply, then please delete this e-mail, together with any attach=
  ments 
  to it, from your computer.</FONT></EM></FONT><FONT size=3D2> </FONT></P><=
  /BODY>
  </HTML>
  
  ------_=_NextPart_002_01C824BD.9AAA8246--
  
  ------_=_NextPart_001_01C824BD.9AAA8246
  Content-Type: application/octet-stream;
  	name="list-arrays.pvs"
  Content-Transfer-Encoding: base64
  Content-Description: list-arrays.pvs
  Content-Disposition: attachment;
  	filename="list-arrays.pvs"
  
  bGlzdF9hc19hcnJheXNbVDpUWVBFXSA6IFRIRU9SWQpCRUdJTgoKICBMaXN0IDogVFlQRSA9IFsj
  CiAgICBsZW5ndGggOiBuYXQsCiAgICBlbGVtcyAgOiBbYmVsb3cobGVuZ3RoKS0+VF0KICAjXQoK
  ICBsIDogVkFSIExpc3QKICB0IDogVkFSIFQKCiAgTnVsbD8obCk6Ym9vbCA9IGxlbmd0aChsKSA9
  IDAKCiAgTnVsbCA6IExpc3QgPSAoIwogICAgbGVuZ3RoIDo9IDAsCiAgICBlbGVtcyAgOj0gTEFN
  QkRBKHg6YmVsb3coMCkpOmVwc2lsb24oZW1wdHlzZXRbVF0pCiAgIykKCiAgQ29ucz8obCk6Ym9v
  bCA9IG5vdCBOdWxsPyhsKQoKICBDb25zKHQsbCk6IExpc3QgPSBsIFdJVEggWwogICAgYGxlbmd0
  aCAgICAgICAgICA6PSBsYGxlbmd0aCsxLAogICAgYGVsZW1zKGxgbGVuZ3RoKSA6PSB0CiAgXQoK
  RU5EIGxpc3RfYXNfYXJyYXlzCgpsaXN0c19hcnJheXNbVDpUWVBFXSA6IFRIRU9SWQpCRUdJTgog
  IAogIElNUE9SVElORyBsaXN0X2FzX2FycmF5c1tUXSwKICAgICAgICAgICAgbGlzdFtUXXt7IGxp
  c3QgIDo9IExpc3QsCiAgICAgICAgICAgICAgICAgICAgICBudWxsPyA6PSBOdWxsPywKICAgICAg
  ICAgICAgICAgICAgICAgIGNvbnM/IDo9IENvbnM/LAogICAgICAgICAgICAgICAgICAgICAgbnVs
  bCAgOj0gTnVsbCwKICAgICAgICAgICAgICAgICAgICAgIGNvbnMgIDo9IENvbnMgfX0KRU5EIGxp
  c3RzX2FycmF5cwoKCgoK
  
  ------_=_NextPart_001_01C824BD.9AAA8246--

How-To-Repeat: 

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