We-Assert-Proof is an assert utility for use in internally verifying statements inside scripts at runtime. One potential goal is to catch what would otherwise be silent errors, or perhaps even to mathematically prove that an algorithm has functioned as expected. See also We-Assert (https://github.com/xerocross/we-assert).
We-Assert-Proof depends on Vulcan, Version 0.4.0, (https://github.com/RyanMarcus/vulcan), which is old but appears to be stable. Aside from that dependency, it is a one-man project written and maintained by Adam Cross. If I say "we", really I'm just referring to myself.
This project was stale for a long while, but as of June 2023 I have updated its dependencies and made it presentable for possible future development. There are problems, and I haven't yet figured out how to actually use Vulcan here to implement mathematical proofs into code. That is something I want to do eventually.
We-Assert-Proof is basically a fork of We-Assert V3 (https://github.com/xerocross/we-assert). I found the license of Vulcan burdensome and the assertion functionality of We-Assert does not need Vulcan, so I removed the dependency from We-Assert as of V4 and made We-Assert-Proof a separate project. See We-Assert for the assertion functionality of We-Assert-Proof without Vulcan and without the burdensome license.
We-Assert-Proof is published to NPM as we-assert-proof. Standard importing would look like this.
import WeAssertProof from "we-assert-proof"
The source code is at https://github.com/xerocross/we-assert-proof.
To install execute npm install.
We-Assert-Proof is written in TypeScript. The package includes a test suite and a script for running it. Use npm test to run the test suite, which is written using Jest.
Note the restrictive copyleft license. That was not my decision. I prefer to use the MIT license, but because Vulcan uses the highly restrictive GNU AFFERO GENERAL PUBLIC LICENSE, and because Vulcan is bundled with We-Assert-Proof, I was required to use a compatible license, so I used the same one. For software with just the assertion functionality of We-Assert-Proof, see my other project we-assert (v4+) instead: We-Assert https://github.com/xerocross/we-assert.
import WeAssertProof from "we-assert-proof";
var we = WeAssertProof.build();
Here we is not a singleton. You can build as many as you want, and each has its own scope and each can be configured independently.
The most basic usage is the that(statement, message) function. For example
we.assert.that(x < y, "x < y");
We recommend writing messages that are positive assertions representing the calculation—not an error message to be thrown upon failure.
If the statement evaluates false, the weAssert handler will be called. The handler should be a function of the form handler : (message) => {...}. To define such a function, we use we.setHandler as in this example.
we.setHandler((message) => {
throw new Error(`The following assertion failed: ${message}`);
});
Note how in the handler we have translated the positive assertion into an error message about exactly which assertion failed. Of course instead of throwing an error you could just swallow it, or log it, or throw the error and log it. You get the idea. We-AssertProof is agnostic to handling the failure of assertions. Handle it however you want.
We can set the level using any of the following:
we.setLevel("DEBUG"), we.setLevel("WARN"), or we.setLevel("ERROR"). The default is "ERROR".
A specific assertion can be assigned a level using the atLevel function as in this example.
we.assert.atLevel("WARN").that(statement, message)
When using this construction, the statement will only be evaluated if the level given ("WARN") is greater than or equal to the threshhold level defined using weAssert.setLevel. The order is DEBUG < WARN < ERROR. Thus, for example, if we set weAssert.setLevel("ERROR") and then execute
we.assert.atLevel("WARN").that(false, "test")
the handler will not be called and nothing will happen because WARN is not greater than or equal to the current level ERROR.
By contrast, if you call
we.assert.that(false, "test")
then levels play no role in the assertion. It will be treated as an error and it will go to the handler.
You can define arbitrary data types so long as you can pass in a function that evaluates boolean to check whether any input passes or fails. The predicate defines the data type.
The usage pattern is we.assert.typeOf(data).is(_tyepstring_, _message_) to validate a given element data.
we.define.type("natural", (x) => isNaturalNumber(x));
we.assert.typeOf(x).is("natural", "x is a natural");
The we instance does not come with any predefined types. If you want to use the standard types you can define them in your we instance by, for example, executing this:
we.define.type("number", (x) => typeof x === "number");
we.define.type("array", (x)=> Array.isArray(x));
You can also check a data element and get a boolean directly like this. This has no side effects. If false, the handler will not be called.
let x = 12;
we.define.type("natural", (x) => isNaturalNumber(x));
expect(we.check.typeOf(x).is("natural")).toBe(true);
Putting these things together, we can define something like this:
we.define.type("natural", (x) => isNaturalNumber(x));
we.define.type("natural[]", function (x) {
if (!Array.isArray(x)) {
return false;
} else {
for (let i = 0; i < x.length; i++) {
if (!we.check.typeOf(x[i]).is("natural")) {
return false;
}
}
return true;
}
});
expect(we.check.typeOf([2, 4, 7.5, 10]).is("natural[]")).toBe(false);
We should probably have different, independent handlers for the different error levels, for DEBUG, WARN, AND ERROR. I might do that later.
I'm playing with some ideas related to logical proof. I would really like to wire automated proofs into this thing, but I have not cracked it yet.
There is more functionality in We-Assert-Proof that I have not documented here yet. I need to add more documentation to this readme document.