Re: Integrated theorem prover in compiler

Walter Banks <walter@bytecraft.com>
Wed, 19 Aug 2009 15:37:30 -0400

          From comp.compilers
Related articles
Integrated theorem prover in compiler cdegouw@gmail.com (- -) (2009-08-19)
Re: Integrated theorem prover in compiler bmd@cs.kuleuven.be (bart demoen) (2009-08-19)
Re: Integrated theorem prover in compiler walter@bytecraft.com (Walter Banks) (2009-08-19)
Re: Integrated theorem prover in compiler pertti.kellomaki@tut.fi (Pertti Kellomaki) (2009-08-20)
Re: Integrated theorem prover in compiler torbenm@pc-003.diku.dk (2009-08-20)
Re: Integrated theorem prover in compiler gneuner2@comcast.net (George Neuner) (2009-08-20)
Re: Integrated theorem prover in compiler bobduff@shell01.TheWorld.com (Robert A Duff) (2009-08-20)
Integrated theorem prover in compiler MSITARA@clemson.edu (Murali Sitaraman) (2009-10-16)
| List of all articles for this month |
From: Walter Banks <walter@bytecraft.com>
Newsgroups: comp.compilers
Date: Wed, 19 Aug 2009 15:37:30 -0400
Organization: Compilers Central
References: 09-08-030
Keywords: theory, optimize
Posted-Date: 20 Aug 2009 10:25:27 EDT

- - wrote:


> 2) There is no need to check the assertions in a program at run-time
> anymore if they already have been checked statically


On this one small point we had support for user defined assertions in
a compiler that were checked statically when they could and left as
part of the source level debugging for the the emulation or simulation
environment to check. We found it to be a bad idea for several
reasons.


1) The developers were distracted for the the application algorithms
and tended to make more implementation errors.


2) As the application evolved some of the initial assumptions changed
and later in the development process the false failures were seen as
errors in the changes. Rather than analyse the application code the
assertions were treated as independent "correct" information.




Regards,


Walter..


--
Walter Banks
Byte Craft Limited
http://www.bytecraft.com

Post a followup to this message

Return to the comp.compilers page.
Search the comp.compilers archives again.