Differences
This shows you the differences between two versions of the page.
Both sides previous revision Previous revision Next revision | Previous revision Next revision Both sides next revision | ||
sav08:homework01 [2008/02/23 21:18] piskac |
sav08:homework01 [2008/05/29 11:47] barbara typo |
||
---|---|---|---|
Line 24: | Line 24: | ||
} | } | ||
</code> | </code> | ||
- | You should be able to save this file as BinarySearchTree.scala, compile it with "scalac BinarySearchTree.scala", run it witn "scala BinarySearchTree", and obtain as a result "Inside". | + | You should be able to save this file as BinarySearchTree.scala, compile it with "scalac BinarySearchTree.scala", run it with "scala BinarySearchTree", and obtain as a result "Inside". |
* for fun, test [[piVC tool]] and on BinarySearch.pi example (install piVC if needed) | * for fun, test [[piVC tool]] and on BinarySearch.pi example (install piVC if needed) | ||
Line 30: | Line 30: | ||
* you may also wish to check the tutorial and this [[http://afp.sourceforge.net/browser_info/current/HOL/BinarySearchTree/BinaryTree_TacticStyle.html|Binary Search Tree example]] | * you may also wish to check the tutorial and this [[http://afp.sourceforge.net/browser_info/current/HOL/BinarySearchTree/BinaryTree_TacticStyle.html|Binary Search Tree example]] | ||
* for fun, Use formDecider.opt from [[:Jahob system]] to prove the same [[Proofs and Induction#Example|example from class]], as well as the examples in Exercises (install [[:Jahob system]] as well as provers CVC3 and E if needed) | * for fun, Use formDecider.opt from [[:Jahob system]] to prove the same [[Proofs and Induction#Example|example from class]], as well as the examples in Exercises (install [[:Jahob system]] as well as provers CVC3 and E if needed) | ||
+ | * if you log into your EPFL account, the Jahob verifier should be accessible by invoking: | ||
+ | <code> | ||
+ | ~kuncak/software/bin/verify --help | ||
+ | </code> | ||
===== Problem 1 ===== | ===== Problem 1 ===== |