- Learn about the problem of Voronoi diagrams and Fortune's algorithm.
- Write a prototype for this algorithm in Coq's programming language.
- Write a specification for this algorithm in Coq's logical language.
- Perform a proof showing that this algorithm satisfies this specification.
| By | I should ... |
|---|---|
| 3-April | be able to use coq with some confidence. |
| 3-April | have a rough prototype of Fortune's algorithm. |
| 14-April | have an implementation in coq. |
xy-May |
write the specifications. |
| [May | June ] | prove the algorithm is correct. |
Deadline: 23:59, 14th-April .
- Tuesday 9-April : Main goal, redesign the data structure. Bonus, add notations.
- Wednesday : Main goal, handle_site_event. Bonus, decompose circumcenter definition.
- Thursday : Main goal, handle_circle_event. Bonus, debug!
- Friday : Main goal, debugging. Bonus, think about the basic facts.
- Weekend : Leftover from above.