Remerciez-le!

Remerciez @Admin pour avoir partagé cet document gratuitement, de la manière la plus simple, en partageant sur les réseaux sociaux.

User guide 47 Raptor ?? User Guide Please Note the guide has been produced with the intent to show users how to use Raptor refer to the Input Guide for information about Raptor ? s syntax INPUT SCREEN A brief Input Guide has been placed within the program

Raptor ?? User Guide Please Note the guide has been produced with the intent to show users how to use Raptor refer to the Input Guide for information about Raptor ? s syntax INPUT SCREEN A brief Input Guide has been placed within the program to aid users to remind them of some of the syntax required Input Box for the user to de ?ne the program code about which they wish to reason Input Box for the user to de ?ne the post condition of the program code about which they wish to reason Use this button to check if the proof is syntactically correct but not begin the proof Input Box for the user to de ?ne the precondition of the code about which they wish to reason Figure Raptor ? s Input Screen Use this button to check if the proof is syntactically correct and begin the proof If you have used the undo button to return to the input screen you may use this button to resume the proof but not lose the redo history CTHE RULES SEMI RULE Figure Raptor ? s Proof Rule Pane Select a body of more than one program line which involves a semi- colon and click semi The body of program lines is split at the last semi-colon and the two parts of the body are put into their own proof boxes and these boxes are added to the proof An unknown is added at the start of the ?rst box representing the condition that holds before the code execution begins Another unknown is added such that it is the goal of the ?rst box and the assumption to the second box representing a condition which holds between lines of code Another unknown is added to the end of the second box representing the condition which holds after the code has completed ASSIGNMENT RULE Select a program line which represents an assignment and click assg For the goal formula below the assignment which must not be unknown every occurrence of the left hand side of the assignment replaced by its right hand side and added to the proof above the assignment as the new goal CMETHOD RULE Select the assignment statement which is an assignment involving a method call and click method The precondition and post condition of the method call is added to the proof the goal below the method call remains a goal in the proof box the post condition is added as an assumption and the precondition is added as a sub goal in the proof box IF RULE Select an if statement and click if Two new proof boxes are added to the proof the assumption to one box is the condition of the if statement and the assumption of the other is the negated version of the condition Both boxes have the same goal which you must instantiate Similar to the semi rule an unknown is added to the start of both boxes which represents