Re: eliminating array bounds checking overhead

> 1. index an array without checking its bounds


A completely different appraoch to this problem is taken by SPARK,
which is used in safety-critical systems (e.g. EuroFighter,
Lockheed C130J)


In SPARK, we can generate verification conditions (VCs) the proof of
which show that such a run-time check can never fail. (SPARK is an
annotated subset of Ada95 for those of you who've never heard of
it... :-) )


The Examiner (SPARK's static analysis tool) can generate such VCs for
all instances of predefined exceptions. Once the proofs are
discharged, then the compiler can _justifiably_ be instructed to
simply eliminate the checking code.


  - Rod Chapman
      Praxis Critical Systems
      http://www.praxis-cs.co.uk/

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