From: xorque <xorquewasp@googlemail.com>
Subject: Re: Clarification for SPARK postconditions on hidden subprograms.
Date: Fri, 26 Jun 2009 03:41:40 -0700 (PDT)
Date: 2009-06-26T03:41:40-07:00 [thread overview]
Message-ID: <3ac1c20c-32ad-4a89-8661-28625f23a7e8@p23g2000vbl.googlegroups.com> (raw)
In-Reply-To: 189c5cbe-10ce-46c7-89df-dcafcc78cfad@s6g2000vbp.googlegroups.com
Rod Chapman wrote:
>
> Does this function have a global variable by any chance? If so, then
> in annotations, you have to give additional actual parameters.
> See section 3.3 of the Examiner_GenVCs manual.
It does indeed. Checking now...
> We have very deliberately made the _entire_ set of manuals
> available with the GPL release. We hope in future to make
> more tutorial-style information available on-line.
And they are certainly appreciated. They're not particularly
easy to search, however, especially when you're not exactly
sure what you're looking for. I'm really after more practical
examples - the case studies in the manuals are somewhat
abstract and Tokeneer is a bit on the large side. I look forward
to the tutorials.
next prev parent reply other threads:[~2009-06-26 10:41 UTC|newest]
Thread overview: 6+ messages / expand[flat|nested] mbox.gz Atom feed top
2009-06-26 1:43 Clarification for SPARK postconditions on hidden subprograms xorque
2009-06-26 7:55 ` Phil Thornley
2009-06-26 9:29 ` xorque
2009-06-26 10:28 ` Rod Chapman
2009-06-26 10:41 ` xorque [this message]
2009-06-26 10:32 ` Phil Thornley
replies disabled
This is a public inbox, see mirroring instructions
for how to clone and mirror all data and code used for this inbox