Z Specification for the W3C Editor's Draft Core SHACL Semantics
Arthur Ryman
TL;DR
This paper formalizes the W3C Core SHACL Semantics using Z notation, revealing quality issues and confirming the well-foundedness of recursive definitions, paving the way for further validation with executable specifications.
Contribution
It introduces a formal Z notation model for the SHACL semantics, identifying issues and ensuring recursive definitions are well-founded.
Findings
Identified quality issues in the draft specification
Confirmed recursive definitions are well-founded
Established foundation for further formal validation
Abstract
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.
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Code & Models
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
Taxonomy
TopicsModel-Driven Software Engineering Techniques · Formal Methods in Verification · Logic, programming, and type systems