ACTION-32: Formal Specification

• From: Arthur Ryman <arthur.ryman@gmail.com>
• Date: Tue, 23 Feb 2016 21:33:16 -0500
• To: "public-data-shapes-wg@w3.org" <public-data-shapes-wg@w3.org>
• Message-ID: <CAApBiO=NY7iz5Bz=G15i5F7duD9_vFwCuqu1nDp-q0uVZa6YCg@mail.gmail.com>

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