Constraint solving your UIs

Dave Aitken
Feb 25, 2019 · 5 min read

What happens when you take a tool for reasoning about your code, and plug it into the UI of the very code that it’s reasoning about?

It turns out we can do just that. Our core product Imandra is a cloud-native automated reasoning engine for ReasonML and OCaml. Imandra has been primarily designed with formal verification of your code in mind, but part of its toolkit is a powerful constraint solver.

Here’s a simple example from an Imandra REPL session:

# type person = { name: string, age: int };# let beatles_names = [ "John", "Paul", "George", "Ringo" ];# let is_adult_with_a_long_beatles_name = (x : person) : bool =>
List.exists(((n : string) => n == x.name), beatles_names) &&
String.length(x.name) > 4 &&
x.age > 18;
# instance((a_person : person) => is_adult_with_a_long_beatles_name(a_person));1 base ground recursive instance
Instance (after 3 steps, 0.038s):
let a_person = {name = "George"; age = 19}
[✔] Instance found.
module CX : sig val a_person : person end

We define a type and then ask Imandra to generate an instance of it where the passed constraint function holds true.

When invoked, Imandra interprets your code and constraint functions with their underlying mathematical semantics in order to solve the constraints (as
opposed to randomly generating values and subsequently filtering them).

We also get the generated value back as something we can compute with:

# CX.a_person.age;
- : int = 19
# is_adult_with_a_long_beatles_name(CX.a_person);
- : bool = true

This REPL-based interactive workflow can be pretty handy for exploring and experimenting with your code and its functions as you’re writing it. But let’s kick things up a notch and visualise this another way.

Understanding your UIs

In previous posts, we’ve talked about verifying React component logic written in ReasonML as part of our Verified React project. Summarizing those posts briefly, we can write core UI logic as a ‘pure’ state machine that Imandra can reason about, then delegate to it from the reducer function of a React component shell.

We can then ask Imandra for instances of our component state, and display that state instance in the UI component itself. Here’s an example of a TodoMVC app we’ve put together where we’re doing just that:

The input on the left is accepting our constraint function (the function we passed to instance in our REPL example), we then send it to Imandra over HTTP and render the returned instance via the UI.

We’ve pre-loaded a couple of helper variables and functions to help out with writing the constraints, but any expression based on the core logic would work — the rest of the generation is based purely on automatic analysis of the code of the component itself.

The final example constraint in the clip above also demonstrates how we can evolve the component’s initialState using its own update function, which can be useful for getting a visual handle on how things are working, and what particular actions do.

Currently when viewing component instances the component has to be modified very slightly so that the wrapping instance querying component can pass instances of the state through to it as a prop. Ideally we’d tap into the framework itself and inject the state in directly, and that’s something we want to look at next, but for now this shows the general idea pretty well!

You can try this example out by installing Imandra, cloning the verified-react repo and following the setup instructions in the README. There’s also another example of generating instances of TicTacToe in the same repo.

Constraint solving for profit

Here’s an example of that as part of a mini seating planner app:

Pairings define either whether people are indifferent to each other (neutral face), want to sit next to each other (happy face), or want to sit apart (sad face), and the visualisation below shows the table assignments for each person.

As the variables involved in the constraints are changed by toggling the UI, we send them up to Imandra as they’re changed. Imandra loads them in, and they’re examined alongside a pre-loaded constraint function to generate instances of valid seating arrangements. We then display these seating instances in the UI.

There is naturally a bit of overhead in the translation from code to raw
constraint expressions, vs hand written constraint expressions written with your domain in mind, but we can play around with different ways of expressing the same constraints to find the most optimal approach. However even a naive encoding can be a great starting point when experimenting.

What’s next?

Watch this space!

If any of this sounds interesting to you we’d love to hear from you - come and chat with us in Discord, or check out Imandra. We’ll also be at ReasonConf in April, so come and talk to us there!

Imandra

Reasoning as a Service @ www.imandra.ai

Medium is an open platform where 170 million readers come to find insightful and dynamic thinking. Here, expert and undiscovered voices alike dive into the heart of any topic and bring new ideas to the surface. Learn more

Follow the writers, publications, and topics that matter to you, and you’ll see them on your homepage and in your inbox. Explore

If you have a story to tell, knowledge to share, or a perspective to offer — welcome home. It’s easy and free to post your thinking on any topic. Write on Medium

Get the Medium app

A button that says 'Download on the App Store', and if clicked it will lead you to the iOS App store
A button that says 'Get it on, Google Play', and if clicked it will lead you to the Google Play store