Purpose: consider the costs and benefits of Formal Methods, reflect on potential applications of the tools used in class
Write a short essay (2-3 pages, double spaced) on the techniques used by Praxis—Z and Spark—to reduce defect levels [Ross06] (including sidebar on p. 40). Explain how Alloy and JML might be used in a similar way (assuming the JML tools were moved from research-quality to industry-quality). Discuss the additional costs and benefits of this approach as compared to more traditional software development and maintenance practices.
I’ll grade your work based on completeness, clarity, conciseness, and correct use of English (including spelling and punctuation).