* Martin Uecker wrote: > Die Frage ist doch, was f�r Eigenschaften man verifiziert, nicht in > welchen System. Deine Beispiele (Division durch 0, Bereichs�berschreitungen) > sind normalerweise Eigenschaften, die sehr leicht zu beweisen sind.
Dann haben wir aneinander vorbei geschrieben. Mir ging es erstmal um die Abwesehenheit von solchen Laufzeitfehler. Das ist IMHO zwar nicht trivial, besonders, wenn man zeigen mu�, da� Grenzen f�r Ausdr�cke eingehalten werden m�ssen oder keine Aliasierungseffekte auftreten k�nnen. Denn der Aufwand von diese Punkte zu beweisen oder gleich allgemeinere Spezifikationsregeln am Code nachzupr�fen unterscheidet sich nicht, sobald man die Spec hat.
