Introduction
SpecLogician is Imandra’s AI assistant for Behaviour-Driven Development (BDD). It can analyze informal specifications written in plain English and turn them into unambiguous, machine-checkable models.
Behaviour-Driven Development
SpecLogician works with natural language specifications written in the Gherkin syntax.
Gherking specs, aka features, are represented as a sequence of user stories following a Given-When-Then structure. Each user story, also called scenario, describes, in largely informal natural language, a particular use case of the system being specified. Gherking specifications are typically used in conjunction with the Cucumber tool, which is used to generate unit tests from scenarios.
Why you should be using SpecLogician
Tools like Cucumber are valuable because they deal with informal specs, which can be read and written by non-technical as well as technical people.
However, while the mere activity of writing a spec might be easier, it does not mean that informal natural language specs are any easier to get right. Our experience with formal methods teaches us that humans are prone to errors, and that having a computer check our work is invaluable. This is why so many system specification language (like Imandra Protocol Language (IPL) or NASA’s fret tool) are based on formal languages that can be understood by automated tools.
SpecLogician bridges the gap between informal and formal specs, bringing the best of both worlds.
With SpecLogician, the user writes a plain-English specification with Gherkin syntax, using informal natural language. SpecLogician then uses LLM technology and agentic workflows to automatically translate the user’s natural language spec into a more formal and rigorous intermediate representation, that we call FormalSpec. You can think of FormalSpec as a more constrained but completely unambiguous and executable alternative to Gherkin.
SpecLogician allows to develop specs iteratively, either by modifying the source natural language spec, or the formalized FormalSpec directly. SpecLogician will take care of keeping them in sync, by automatically applying user edits from one version of the spec to the other.
The value of the formal specs generated by SpecLogician is in that their are formal and machine readable, which allows automated tools like the Imandra theorem prover to reason about their properties and extract useful artifacts like tests.
In summary, here’s what SpecLogician can do for you:
- Assist in the development of requirements, by ensuring that your specs are logically coherent and include all necessary assumptions
- Verify properties about the specification using theorem proving, helping to uncover missing execution paths or unexpected edge cases
- Automate test case generation
Generating IPL models
IPL is Imandra’s language for expressing system specifications, in the form of state machines. SpecLogician can use its FormalSpec representation of the user’s spec to automatically generate a correponding state machine representation in the form of an IPL model. This process is made possible by FormalSpec’s formality and lack of ambiguity, which allows a direct and deterministic translation into IPL.
IPL is an example of a language which provides a Machine-Reasonable API. This means that the model is not only machine readable, but also it is possible to reason about a model written in the language. SpecLogician’s ability to translate informal specs into IPL model thus opens a whole realm of possible ways to formally reason about requirements, without sacrificing the accessibility of informal natural language specs.
State space exploration and reachability analysis
Much of SpecLogician’s automated reasoning power comes from Region Decomposition, one of the core features of the ImandraX theorem prover. Region decomposition allows to decompose behavior of models into a finite number of symbolic regions where each region contains a set of constraints on the inputs and a description of the outcome (called invariant result). In other words, Region Decomposition allows to take a model and identify all distinct behaviors (or edge cases). An edge case corresponds to a “region” of the model’s state space. A state space corresponds to all possible inputs and outputs. When we define this “region” we do so by describing what the inputs will look like through a list of constraints. Each region then contains “invariant” result which describes what the model will output if the inputs satisfy that region’s constraints. When ImandraX generates these regions, it does so with mathematical precision.
By running Imandra’s region decomposition on the specs it formalizes, SpecLogician can explore the state space of the system being specified. This is of great help when determining whether the specification accurately covers all aspects of the target system. In particular, it helps figuring out
- paths that are not covered by the spec, but should
- unexpected edge cases that the spec allows, but shouldn’t
Test case generation
SpecLogician supports Behaviour-Driven Development (BDD) workflows, with its ability to automatically generate test cases from specifications. Compared to tools like Cucumber, SpecLogician’s test generation capabilities go beyond simply generating unit tests that correspond 1-to-1 to scenarios/user stories.
SpecLogician uses ImandraX’s Region Decomposition under the hood, which means it can generate high-coverage tests exercising all logically feasible execution paths. Compared to other state machine-based test generation tools that generate tests based on a purely syntactic analysis of the system (thus disregarding runtime behaviour), SpecLogician uses Region Decomposition to run a semantic analysis of the execution paths described by the user’s spec, leading to a more comprehensive and mathematically sound test suite that covers edge cases that might otherwise be missed by traditional testing approaches.