comp.lang.ada
 help / color / mirror / Atom feed
From: Rod Chapman <roderick.chapman@googlemail.com>
Subject: Re: SPARK
Date: Fri, 14 May 2010 02:32:05 -0700 (PDT)
Date: 2010-05-14T02:32:05-07:00	[thread overview]
Message-ID: <1fa6a7b3-ae22-4223-bd11-bbf2dff411c7@p2g2000yqh.googlegroups.com> (raw)
In-Reply-To: 30e0a8bd-e6f8-425c-9423-6eba7f35972d@n15g2000yqf.googlegroups.com

> As you are discovering, the documentation for the optional proof
> assertions in SPARK is not easy to find (it is spread across several
> documents, and rather scattered within those documents).

Noted.  For SPARK Pro 9.0, we merged all the Proof material
into one manual and gave it the rather more obvious title "Proof
Manual".
We also produced a one-page clickable index to _all_ the manuals,
which has also proven useful.
 - Rod Chapman, SPARK Team



  reply	other threads:[~2010-05-14  9:32 UTC|newest]

Thread overview: 61+ messages / expand[flat|nested]  mbox.gz  Atom feed  top
2010-05-12 22:55 SPARK Yannick Duchêne (Hibou57)
2010-05-13  0:52 ` SPARK Yannick Duchêne (Hibou57)
2010-05-13  3:06 ` SPARK Yannick Duchêne (Hibou57)
2010-05-13  9:28   ` SPARK stefan-lucks
2010-05-13 16:48     ` SPARK Yannick Duchêne (Hibou57)
2010-05-15 13:09       ` SPARK Peter C. Chapin
2010-05-14 22:55   ` SPARK Yannick Duchêne (Hibou57)
2010-05-13  4:00 ` SPARK Yannick Duchêne (Hibou57)
2010-05-13 16:54 ` SPARK Yannick Duchêne (Hibou57)
2010-05-13 17:15   ` SPARK Rod Chapman
2010-05-13 19:43     ` SPARK Yannick Duchêne (Hibou57)
2010-05-13 20:05       ` SPARK Rod Chapman
2010-05-13 21:43         ` SPARK Yannick Duchêne (Hibou57)
2010-05-14 14:47         ` SPARK Yannick Duchêne (Hibou57)
2010-05-14  1:20 ` SPARK Yannick Duchêne (Hibou57)
2010-05-14  4:15   ` SPARK Yannick Duchêne (Hibou57)
2010-05-14  8:17     ` SPARK Phil Thornley
2010-05-14  9:32       ` Rod Chapman [this message]
2010-05-14 14:20       ` SPARK Yannick Duchêne (Hibou57)
2010-05-14  3:07 ` SPARK Yannick Duchêne (Hibou57)
2010-05-14  3:26   ` SPARK Yannick Duchêne (Hibou57)
2010-05-14  8:11   ` SPARK Phil Thornley
2010-05-14 14:28     ` SPARK Yannick Duchêne (Hibou57)
2010-05-14 21:45 ` SPARK Yannick Duchêne (Hibou57)
2010-05-15 16:41 ` SPARK Yannick Duchêne (Hibou57)
2010-05-15 18:00   ` SPARK Yannick Duchêne (Hibou57)
2010-05-15 18:14   ` SPARK Yannick Duchêne (Hibou57)
2010-05-15 19:08     ` SPARK Yannick Duchêne (Hibou57)
2010-05-15 20:23       ` SPARK Yannick Duchêne (Hibou57)
2010-05-16 18:13         ` SPARK Peter C. Chapin
2010-05-17  0:59           ` SPARK Yannick Duchêne (Hibou57)
2010-05-16 18:17         ` SPARK Phil Thornley
2010-05-17  1:24           ` SPARK Yannick Duchêne (Hibou57)
2010-05-15 18:43   ` SPARK Phil Clayton
2010-05-15 19:12     ` SPARK Yannick Duchêne (Hibou57)
2010-05-15 21:02       ` SPARK Phil Clayton
2010-05-15 22:48 ` SPARK Yannick Duchêne (Hibou57)
2010-05-16  1:48   ` SPARK Yannick Duchêne (Hibou57)
2010-05-16  1:53     ` SPARK Yannick Duchêne (Hibou57)
2010-05-16  5:28 ` SPARK Yannick Duchêne (Hibou57)
2010-05-18 18:01   ` SPARK Yannick Duchêne (Hibou57)
2010-05-19  8:09     ` SPARK Phil Thornley
2010-05-19 20:38       ` SPARK Simon Wright
2010-05-19 21:27         ` SPARK Yannick Duchêne (Hibou57)
2010-05-20  6:21           ` SPARK Simon Wright
2010-05-20  6:58             ` SPARK Yannick Duchêne (Hibou57)
2010-05-20 21:51               ` SPARK Simon Wright
2010-05-19 21:35       ` SPARK Yannick Duchêne (Hibou57)
  -- strict thread matches above, loose matches on Subject: below --
2009-06-10  9:47 SPARK Robert Matthews
2004-08-18 23:46 timeouts Brian May
2004-08-19  3:40 ` timeouts Steve
2004-08-22  4:18   ` timeouts Brian May
2004-08-22 12:54     ` timeouts Jeff C,
2004-08-26  1:28       ` timeouts Brian May
2004-08-26 13:34         ` timeouts Steve
2004-08-26 14:02           ` timeouts Georg Bauhaus
2004-08-26 23:03             ` SPARK Brian May
2004-08-27 10:11               ` SPARK Georg Bauhaus
2001-08-08  9:46 SPARK Soeren.Henssel-Rasmussen
2001-08-08 20:04 ` SPARK McDoobie
2001-08-06 16:49 SPARK programmer
2001-08-07  7:04 ` SPARK Hambut
2001-08-07  7:18 ` SPARK Hambut
2001-08-07  8:37 ` SPARK Peter Amey
2001-08-07 14:42   ` SPARK McDoobie
2001-08-09 12:36   ` SPARK Peter Amey
2001-08-14  3:14   ` SPARK Prof Karl Kleine
2001-08-14 10:25     ` SPARK Rod Chapman
replies disabled

This is a public inbox, see mirroring instructions
for how to clone and mirror all data and code used for this inbox