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

Q: list

To: pvs-help@csl.sri.com
Subject: Q: list
From: Kong Woei Susanto <susanto@dcs.gla.ac.uk>
Date: Wed, 19 May 1999 15:18:02 +0000
Sender: susanto@dcs.gla.ac.uk

Hi,

I wonder why I can not prove this:

[-1] (x!1=(:(# name:=(#
portName:="o",instanceName:=instanceName(y!1)#),val:=Sig0 #):))
  |-------
[1] outPorts(x!1)


  |-------
[1] outPorts((: :))


  |-------
{1} CASES (: :) OF null: TRUE, cons(hd, tl): outPort(hd) AND
outPorts(tl) ENDCASES


Thanks,

-- 
Kong Woei Susanto
Department of Computing Science - University of Glasgow
17 Lilybank Gardens, Glasgow G12 8RZ, Scotland, United Kingdom.
e-mail: susanto@dcs.gla.ac.uk Ph: +44-141-3304454  fax:+44-141-3304913

Prev by Date: problem of pvs to z specification
Next by Date: Q; list (additional information)
Prev by thread: Re: Q; list (additional information)
Next by thread: problem of pvs to z specification
Index(es):
- Date
- Thread