From: "Yannick Duchêne (Hibou57)" <yannick_duchene@yahoo.fr>
Subject: Re: SPARK
Date: Sun, 16 May 2010 07:28:16 +0200
Date: 2010-05-16T07:28:16+02:00 [thread overview]
Message-ID: <op.vcr9heg2ule2fv@garhos> (raw)
In-Reply-To: op.vcl6900wule2fv@garhos
Request for confirmation.
In Praxis's documentations, there is a file named Checker_Rules.pdf, title
is “SPADE Proof Checker Rules Manual”, which list Checker's built-in
rules. I do not see any reason why the Examiner/Simplifier would have a
different rules set than the Checker, so I suppose this rules set is also
the one used by the Examiner/Simplifier. I would just want to be sure :
someone can confirm ?
If it is, this may explain why I meet some troubles proving one thing with
real arithmetic (yes, I know real arithmetic is not safe and I must care,
but this is just an exercise...)
--
There is even better than a pragma Assert: a SPARK --# check.
Wanted: if you know about some though in the area of comparisons between
SPARK and VDM, please, let me know. Will enjoy to talk with you about it.
next prev parent reply other threads:[~2010-05-16 5:28 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 ` SPARK Rod Chapman
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 ` Yannick Duchêne (Hibou57) [this message]
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