Calculational proof where chain of equality is established to show first and last statement are equal is an elegant way to write proof. For example Dafny has support for writing calculational proof using calc. Following proof shows that App…
In previous blog we looked into why TLA+ specification enforces SI (stuttering insensitivity) and how verifying liveness assertion required us to add fairness condition in spec. In this blog we will model timer displaying minute in Dafny us…
Recently I came across this nice puzzle - Haunted. These days my impulse when presented with puzzle is throw Answer Set Programming on it. To get idea of ASP follow this blog which solves another puzzle which has somewhat straightforward en…
Rosette is a solver-aided language. Its documentation has good overview of how it can be used. It has been used to find bug in eBPF, reasoning about SQL equivalence and in many other ways. I have covered Rosette previously in this blog by u…
Note: This blogpost is heavily inspired from this wolfram community article. Whether a single geometrical shape exists that can tile plane aperiodically was open problem until recently. Since discovery of hat and related shapes we know answ…
Let’s say you want to specify Timer in TLA+ which counts down 5 minutes of time. Code listed above shows TLA+ specification for the same, assuming you want minutes to decrease by 1 in single step until it reaches 0. Ideally you want SPEC to…
Hitori is logic puzzle with goal to color some cells black such that ASP (Answer Set Programming) is declarative approach to problem solving. Idea is to give description of problem you are solving instead of giving algorithm (how to solve).…
Permutations of multiset can be generated in lexicographical order. Wikipedia has description of how such algorithm works. Let’s implement next_permutation in Dafny which given array as input returns next permutation. Fun and challenging pa…
As part of production monitoring it is standard practice to measure p95, p99 latencies. We also want to query these metrics over dynamic time range. What is p99 latency over last 3 hours? What is p99 latency over last 5 minutes? One option
In this we will implement and verify solution of two sum problem. Two sum problem asks for a pair of indices in sorted sequence such that elements at those indices add up to given sum. It is given that such indices exist. Linear time implem…
Would n’t it be interesting if programming language is aided with SMT solvers. Rosette is such language. Using SMT solvers Rosette can verify that programs comply their specifications, synthesis programs given specifications, find counterex…