[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

*To*: pvs-help@xxxxxxxxxxx*Subject*: [PVS-Help] Simple (?) question on PVS - constants of functions ofother constants*From*: "David A. Wheeler" <dwheeler@xxxxxxxxxxxx>*Date*: Tue, 22 May 2007 16:30:26 -0400 (EDT)*List-Help*: <mailto:pvs-help-request@csl.sri.com?subject=help>*List-Id*: PVS-Help <pvs-help.csl.sri.com>*List-Post*: <mailto:pvs-help@csl.sri.com>*List-Subscribe*: <http://lists.csl.sri.com/mailman/listinfo/pvs-help>,<mailto:pvs-help-request@csl.sri.com?subject=subscribe>*List-Unsubscribe*: <http://lists.csl.sri.com/mailman/listinfo/pvs-help>,<mailto:pvs-help-request@csl.sri.com?subject=unsubscribe>*Reply-To*: dwheeler@xxxxxxxxxxxx*Sender*: pvs-help-bounces+archive=csl.sri.com@xxxxxxxxxxx

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

- Prev by Date:
**Re: [work] [PVS-Help] Flatten VS Split** - Next by Date:
**Re: [PVS-Help] Simple (?) question on PVS - constants of functions ofother constants** - Prev by thread:
**Re: [PVS-Help] Simple (?) question on PVS - constants offunctions of other constants** - Next by thread:
**Re: [PVS-Help] Simple (?) question on PVS - constants of functions ofother constants** - Index(es):