Second Project
Deadline
The deadline of the second project is
18th of December, 2019FAQ
- For the reverse copy challenge, do I have to support newline characters across different systems?
NO. As long as it works in your system, it's acceptable. - What can I assume for the reverse copy challenge (and what should I verify)?
The main goal of the exercise is to verify two properties: i) that your reverse method is indeed reversing its argument and ii) the lines in the new file are the reverse of the original file.
You can define functions/methods to extract lines and concatenate lines (unlines) without verifying their properties. You can also define a predicate that states when two file streams are "line-reversed" in terms of these functions (e.g. two file streams s1 and s2 are "line reversed" when s1 == unlines(reverse(lines(s2)))). You can then use this predicate in your specifications. The file Challenge1-example.dfy has some code examples that you are free to use. The code given does not work for files with empty lines (e.g. if the file ends with \n). You are welcome to fix this, but it is not necessary. The focus of the specification exercise is on points i) and ii) above.
Attachments
