Re: [PVS-Help] Simple (?) question on PVS - constants of functions ofother constants

[Sam Owre <owre@xxxxxxxxxxx>]

Hi David,

The problem is that you've given a type where an expression is expected.
You could do something like

  comp: TYPE = [Compiler: CIO, Source: SRC -> CIO]

  cmp: comp

  Stage1: CIO = cmp(T, sA)

Regards,
Sam Owre

David A. Wheeler <dwheeler@dwheeler.com> wrote:

> From: "David A. Wheeler" <dwheeler@dwheeler.com>
> To: pvs-help@csl.sri.com
> Date: Tue, 22 May 2007 16:30:26 -0400 (EDT)
> Subject: [PVS-Help] Simple (?) question on PVS - constants of functions of
>  other constants
> Reply-To: dwheeler@dwheeler.com
> 
> Hi - I'm a new PVS user, and I'm trying to translate a hand-created proof into PVS.  But almost immediately I'm running into trouble; I can't seem to define constants that are the results of functions on other constants.  Instead I get "No resolution for comp with arguments of possible types..." error messages.
> 
> What's wrong in the tiny snippet below?  I presume it's really obvious, but I don't know what it is.
> 
> I'm basically trying to prove some assertions related to compiling code.  I do NOT want to define the specific compilation function. Instead, I need to make general assertions like "if a function that compiles something meets properties <P>, then claims <C> will be true."
> 
> Thanks.
> 
> --- David A. Wheeler
> 
> ================================================
> 
> problem: THEORY
>  BEGIN
>   SRC: TYPE % Any Source code has this type
>   CIO: TYPE % Any input/output of a compilation other than SRC
> 
>   % A compilation step is a function that accepts a CIO (the compiler)
>   % and SRC (the source code), and produces a CIO (the compiled result)
>   comp: TYPE = [Compiler: CIO, Source: SRC -> CIO]
> 
>   sA: SRC
>   T: CIO  % T is a compiler
> 
>   Stage1: CIO = comp(T, sA)
>   % This will produce this error message:
>   % Expecting an expression
>   % No resolution for comp with arguments of possible types: 
>   %  T : CIO
>   %  sA : SRC
> 
>   % This doesn't work either:
>   Stage1: CIO
>   Stage1_is: AXIOM Stage1 = comp(T, sA)
>   % This will produce this error message:
>   % Expecting an expression
>   % No resolution for comp with arguments of possible types: 
>   %  T : CIO
>   %  sA : SRC
> 
> END problem
>