ACTION-32: Formal Specification

I proposed this action two months ago with the hope that it would help
clarify some issues, including recursion. However, I have been unable
to find the time to do this. I would like to sum up where I got to.

I have previously used Z Notation as a formalization tool. I have
personally found this helpful. However, few people can read or write
Z, so there is little feedback.

A more modern approach is Coq, which is proof-assistant that includes
a formal specification language that is actually a very high-level,
executable, functional programming language. The advantage of Coq
versus Z is that one can actually execute Coq and even generate code
from it. This would let us use it as test oracle.

However, this takes a lot of time, which I do not have. I am therefore
closing this action.

-- Arthur

Received on Wednesday, 24 February 2016 02:33:44 UTC