From: roderick.chapman@googlemail.com
Subject: Re: Reference-oriented language and high-integrity software
Date: 3 Nov 2006 01:43:18 -0800
Date: 2006-11-03T01:43:18-08:00 [thread overview]
Message-ID: <1162546998.925808.52360@h48g2000cwc.googlegroups.com> (raw)
In-Reply-To: <eif0qu$4k8$1@cernne03.cern.ch>
The provision of _sound_ (i.e. no false negatives) and _fast_ aliasing
analysis
a key factor, even in the absence of dynamic memory and garbage
collection.
The soundness (and efficiency) of the information flow analyser
and the VC Generator (which is basically an implementation
of Hoare's assignment axiom) depend on this property.
- Rod, SPARK Team
next prev parent reply other threads:[~2006-11-03 9:43 UTC|newest]
Thread overview: 13+ messages / expand[flat|nested] mbox.gz Atom feed top
2006-11-03 8:03 Reference-oriented language and high-integrity software Maciej Sobczak
2006-11-03 8:58 ` Ludovic Brenta
2006-11-03 9:06 ` Maciej Sobczak
2006-11-03 9:43 ` roderick.chapman [this message]
2006-11-03 11:25 ` Georg Bauhaus
2006-11-03 11:15 ` Ludovic Brenta
2006-11-03 11:59 ` Georg Bauhaus
2006-11-03 12:37 ` Peter Amey
2006-11-03 14:44 ` Martin Krischik
2006-11-03 15:27 ` Dr. Adrian Wrigley
2006-11-03 16:17 ` Simon Wright
2006-11-03 17:30 ` Jean-Pierre Rosen
2006-11-06 7:14 ` Martin Krischik
replies disabled
This is a public inbox, see mirroring instructions
for how to clone and mirror all data and code used for this inbox