Z Notation is a formal model-based language for describing the behavior of a system precisely. Z Notation is an ISO/IEC standard. (International Organization for Standardization; International Electrotechnical Commission). The University of Oxford published this Z Notation Reference Manual.
I found this YouTube video which provides a brief overview describing Z Notation.
Z Notation is based on the rules of mathematics and uses first-order predicate logic. Z Notation is not a programming language, it is not machine-readable. It may seem odd, if you look at Z Notation but it is intended to be read and understood by humans.
The ISO/IEC standard Z Notation specification includes the following examples of the kinds of systems that have been described using Z Notation:
If things are described in a written document, different people reading that document can interpret that document from their perspective. That perspective might be different that the perspective of another person. That leads to the problem of ambiguity in how a system actually works.
That is the problem a formal language such as Z Notation is intended to solve: reducing ambiguity, making descriptions more precise. Formal specifications are precise, concise and unambiguous. Because first-order logic is used a proof can be created which follows the rules of formal logic. Proofs and logic are used in science but the same principles of logic work in business also or any system really.
Deming says: A system must have a goal and everyone needs to understand that goal.
Financial reporting is a system. Financial reporting rules are described in documents. As a result, ambiguity and other things can creep into the system making the system less precise. Articulating the financial reporting rules using something like Z Notation would reduce unintended ambiguity, making financial reporting more precise.
In a blog post that I did a while back I mentioned a paper, An analysis of fundamental concepts in the conceptual framework using ontology technologies; written by Marthinus Cornelius Gerber, Aurona Jacoba Gerber, Alta van der Merwe; which points out ambiguities in financial reporting standards and how those ambiguities can be reduced using formal ontologies.
The folks that wrote that paper used OWL as the syntax for expressing the rules they were looking at. But OWL has a problem. OWL is expressive, but OWL is not expressive enough. For example, mathematical relations cannot be expressed using OWL. Other types of relations cannot be expressed. The easiest way to see this is to look at commercial products such as the Fluent Editor. The Fluent Editor augments the expressive power of OWL (specifically OWL 2 DL) by using SWRL, the Semantic Web Rules Language.
More precisely, Fluent uses what they call "safe SWRL". The fact that Fluent uses only a portion of SWRL which they refer to as "safe SWRL" points out a problem with Z Notation.
Notice that I specifically pointed out that Fluent uses OWL 2 DL. Recall from above that I said that Z Notation is based on first-order predicate logic. First-order predicate logic has some issues in that you can express things that cause computer software to get confused, get lost, or get caught in some sort of infinite loop from which it cannot escape. I discussed these issues in this blog post about Description Logic and in this blog post about "logical catastrophes" or catastrophic failure points.
And so OWL was partitioned into profiles which enable systems to be constructed which avoid specific catastrophic failures. That resulted in one OWL profile called OWL 2 DL which is based on SROIQ Description Logic. That profile is "decidable", as described in the blog post above.
But OWL 2 DL has two other issues. The first issue is that as mentioned, OWL 2 DL does not support expressing mathematical relations. The reason for this is that some mathematics are not "decidable". The second problem is that OWL 2 DL is really hard for business professionals (i.e. virtually impossible) to understand and therefore verify that rules that are articulated are correct.
Am I saying that Z Notation is easy for business professionals to understand? No. The vast majority of business professionals will not take the time to understand that notation. So that is a problem with Z Notation. Another problem with Z Notation is that it is likewise potentially not decidable and you could run into those logical catastrophes. A third issue with Z Notation is that it is not machine-readable.
So what is the right answer when it comes to precisely describing how financial reporting works or how a financial report works? We need that precise description to build software what works as needed and is interoperable with other software which has been created. We need the XBRL-based stuctured information to be understood the same way by all software vendors creating software.
This is what I think:
Why go through all this effort? The reason is, if digital financial reporting (or structured digital reporting, whatever you want to call it) is ambiguous and imprecise it simply will never work. If the details are not worked out correctly then digital financial reports can never be correctly created by business professionals. If business professionals have to rely on information technology professionals to create digital financial reports correctly, digital financial reporting can never really rise to the level that it needs to rise to.
The US SEC and FASB are doing a pretty good job of making XBRL-based public company financial reports to the SEC work. While far from perfect, things are beginning to work, which will make it easy to see why other things do not work, and allows one to see that it is all about the business rules.
It really is pretty basic as I have pointed out before: The only way a meaningful exchange of information can occur is the prior existence of agreed upon technical syntax rules, business domain semantic rules, and workflow rules.
Z Notation helps in this process. While something like the Financial Report Semantics and Dynamics Theory should be expressed in Z Notation; accounting professionals and other business professionals would interact with digital financial reports and the information they contain in ways that they understand and are familiar with.
This is the only way digital financial reporting benefits can be realized. It is the only way expert systems can be constructed that work. This is all about business professionals understanding business rules. Precise rules eliminate ambiguity. Z Notation contributes to people agreeing on the rules.