[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
[PVS-Help] Another rookie question
- To: pvs-help@csl.sri.com
- Subject: [PVS-Help] Another rookie question
- From: Sun Jun <sunj@comp.nus.edu.sg>
- Date: Mon, 2 Feb 2004 16:53:25 +0800 (GMT-8)
- 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>
- Original-Received: from quarter.csl.sri.com (mx0.csl.sri.com [130.107.1.30])by postal.csl.sri.com (8.12.9p2/8.12.9) with ESMTP id i128rnm0039162for <pvs-help@postal.csl.sri.com>; Mon, 2 Feb 2004 00:53:49 -0800 (PST)(envelope-from sunj@comp.nus.edu.sg)
- Original-Received: from mailgate-external2.sri.com (mailgate-external2.SRI.COM[128.18.85.102])by quarter.csl.sri.com (8.12.9/8.12.10) with SMTP id i128rYaV014987for <pvs-help@csl.sri.com>; Mon, 2 Feb 2004 00:53:34 -0800
- Original-Received: (qmail 29997 invoked from network);2 Feb 2004 08:53:28 -0000
- Original-Received: from localhost (HELO mailgate-external2.SRI.COM) (127.0.0.1)by mailgate-external2.sri.com with SMTP; 2 Feb 2004 08:53:28 -0000
- Original-Received: from x86unx3.comp.nus.edu.sg ([137.132.90.3])by mailgate-external2.SRI.COM (SAVSMTP 3.1.2.35) with SMTP idM2004020200532723808for <pvs-help@csl.sri.com>; Mon, 02 Feb 2004 00:53:27 -0800
- Original-Received: from e500a.comp.nus.edu.sg (e500a.comp.nus.edu.sg[137.132.90.23])by x86unx3.comp.nus.edu.sg (8.9.1-20030924/8.9.1) with SMTP id QAA02344for <pvs-help@csl.sri.com>; Mon, 2 Feb 2004 16:53:26 +0800 (GMT-8)
- Original-Received: from sf3.comp.nus.edu.sg(137.132.90.55) bye500a.comp.nus.edu.sg via csmap id 7082; Mon, 02 Feb 2004 16:53:25 +0800 (SGT)
- Original-Received: from localhost (sunj@localhost)by sf3.comp.nus.edu.sg (8.8.5/8.8.5) with ESMTP id QAA15532for <pvs-help@csl.sri.com>; Mon, 2 Feb 2004 16:53:25 +0800 (GMT-8)
- Sender: pvs-help-bounces+archive=csl.sri.com@csl.sri.com
Hi,
I got another rookie question: give a bool expression, how can I do
variable restriction using PVS?
e.g. FORALL (x: int), (y: int): x > 10 & z = x+y
How to find out the constraints on z using PVS? And how to do it in Batch
mode?
yours,
Sun Jun