Recommendation

Unrated

Link

http://www.animal.ahrgr.de/showAnimationDetails.php3?anim=56; http://www.animal.ahrgr.de/showAnimationDetails.php3?anim=110

Delivery Method

Animal Animation

License

Non-Commercial

Language

English; German

Author

Marc-Daniel Haunschild

Institution

TU Darmstadt, Darmstadt, Germany

Project

Animal

RelationshipToProject

PartOfProject

Works

Yes

Description

Verification is a mathematical calculus for proving the correctness of algorithms and programs. It is based on a specification of the expected ("promised") results of a given method, and allows the calculation of the exact conditions under which the promised result can be guaranteed ("precondition"). The animation first motivates the verification approach and interprets the meaning of preconditions before introducing the verification of assignments. Afterwards, the animation presents how one can verify compounds (composite statements typically grouped by { ... } or BEGIN...END), conditional statements via if and while-loops. The animation also offers a simple scheme of where to put what verification part for guaranteeing correct verification.

Evaluation

ActivityLevel

Animation; Step Control; Canned Data

GoodFor

Nothing

Screenshots

Videos

References

HowToUse

For detailed instructions on how to install Animal and run Animal AVs, see: http://www.algoanim.info/Animal2/?q=node/290. Once you have installed the Animal .jar file and downloaded/unpacked the .zip file of Animal animations, you are now ready to run Animal. Run the .jar file to start Animal. Then go to the "Open" menu item, and browse to where you put the animal animations you got in the .zip file. Pick this AV from the list. You can then step through the animation, or use "kiosk mode" to have the steps fed to you at a constant pace.

First Visited

2007-07-21

Last Visited

2010-02-05

Last Updated

1999-05-09

Topic

ProgramVerification

Community

Edit

You may edit this entry if you have an account.