Hello, everyone. One of your classmates has just told me of a small issue in the model I gave you as part of the homework: in the context Search_C0 there are two axioms that appear mistakenly marked as 'theorem', while all of them should appear marked as 'non theorem'. I think I might have clicked on them inadvertently while writing the comments. Bottom line: in the model I gave you, all the axioms and all the invariants should be marked as 'non theorem'. Please make sure this is the case.

You can correct them yourselves. If you haven't downloaded the model yet, I have uploaded another model with these two axioms (hopefully) marked as 'non theorem'.

Best regards,

Manuel

On Sun, 20 Mar 2022 19:21:15 +0100, Manuel Carro manuel.carro@imdea.org wrote:

Hi, all. The second homework for the Correctness by Construction course is available. Please access it at

https://wp.software.imdea.org/cbc/2022/03/20/second-cbc-homework/

Deadline to turn it in: Saturday, April 2nd, 00:01. Send it to me by email.

I recommend to have a look at it before next lecture so that I can answer any question with time enough.

Best regards,