Z Specification for the W3C Editor's Draft Core SHACL Semantics
arXiv:1511.00384v1Has Code
Originality Synthesis-oriented
AI Analysis
This work addresses formal verification for SHACL semantics, which is incremental as it builds on existing draft specifications.
The authors formalized the W3C Draft Core SHACL Semantics using Z notation, identifying quality issues and confirming the well-foundedness of recursive definitions.
This article provides a formalization of the W3C Draft Core SHACL Semantics specification using Z notation. This formalization exercise has identified a number of quality issues in the draft. It has also established that the recursive definitions in the draft are well-founded. Further formal validation of the draft will require the use of an executable specification technology.