Refactoring using mathematical properties of min

Today I refactored a small piece of code.

Before:

$coupon_amount = self::get_coupon_prop( $coupon, 'amount' ) - $already_applied_coupons;

if ( isset( WC()->cart ) ) {
	$coupon_amount = min( WC()->cart->subtotal - $already_applied_coupons, $coupon_amount );
}

if ( $coupon_amount < 0 ) {
	return $discount;
}

After:

$coupon_amount = self::get_coupon_prop( $coupon, 'amount' );

if ( isset( WC()->cart ) ) {
	$coupon_amount = min( WC()->cart->subtotal, $coupon_amount );
}

$coupon_amount -= $already_applied_coupons;

if ( $coupon_amount < 0 ) {
	return $discount;
}

This was intuitive to me, but I wanted to prove that it really does the same thing. For that, we need to use the property .

The usual definition for min is:

Now we can use proof by cases to prove our property which will allow us to confidently refactor our code. There are two cases we can assume:

1. Case :
In this case, , and since from we can conclude that , then .
So, we have that , which proves this case.

2. Case :
In this case, , and since from we can conclude that , then .
So, we have that , which proves this case.

Thus, the property is proven. 🙂

There are also some other properties like and but you can try doing these yourself. Stuff with max is proven analogously.

Advertisements

Dafny – programming language for formal specifications

Dafny is an imperative compiled language that supports formal specification through preconditions, postconditions, loop invariants.

I found out about it from The Great Theorem Prover Showdown, while reading Hacker News one day.

It only seems to target C#, but can automatically prove properties about functions nevertheless.

I finished Dafny Tutorial and it was pretty straight-forward. The tutorial should be easy to follow for anyone with basic knowledge with the C programming language (and mathematical logic). The examples for the Dafny tutorial can be ran from the browser so you do not have to install it locally to go through it.

The reason why I like this programming language is because it seems much simpler than e.g. Coq or Idris that are based on dependent types / Calculus of Constructions (however, note that it still shares some stuff such as algebraic data types, or inductive types).

The tutorial starts with functions, pre-post conditions and assertions, and then proceeds with loop invariants. It proves basic properties for abs/max, etc.

For example, abs takes an integer and produces an integer greater than or equal to zero. Here’s the proof for that:

method Abs(x: int) returns (y: int)
   ensures 0 <= y
{
   y := 0;
}

With ensures we set the post-conditions (alternatively, requires is for pre-conditions). Pretty simple and neat, right? 🙂

Like pre- and postconditions, an invariant is a property that is preserved for each execution of the loop. Here’s an example for an invariant:

method m(n: nat)
{
   var i := 0;
   while i < n
      invariant 0 <= i
   {
      i := i + 1;
   }
}

However if you go through the tutorial you will see by the exercises that the challenge in picking a good loop invariant is finding one that is preserved with each loop execution, but also one that lets you prove what you need.

Finally, example for quantifiers:

method m()
{
   assert forall k :: k < k + 1;
}

The tutorial takes only a couple of hours to finish, and for anyone interested in programming languages like this I highly recommend you go through it 🙂

The conclusion paragraph of the tutorial states it well:

Even if you do not use Dafny regularly, the idea of writing down exactly what it is that the code does is a precise way, and using this to prove code correct is a useful skill. Invariants, pre- and post conditions, and annotations are useful in debugging code, and also as documentation for future developers. When modifying or adding to a codebase, they confirm that the guarantees of existing code are not broken. They also ensure that APIs are used correctly, by formalizing behavior and requirements and enforcing correct usage. Reasoning from invariants, considering pre- and postconditions, and writing assertions to check assumptions are all general computer science skills that will benefit you no matter what language you work in.

For all the tutorial exercises, you can check out my Dafny Git repository.

Lisp interpreter

Here’s a fun exercise:

1. Write a Lisp interpreter in PHP (done a few years ago here)
2. Write a Lisp interpreter in Lisp (done here)

This made me realize why DSLs are much easier to do in a Lisp than in any other programming language.

It has to do with the underlying structure of the programming language. I believe that in a Lisp we have complete control over the abstract syntax tree and it is much easier to tokenize/parse/evaluate. We just read a string and then have a function that recursively evaluates the AST produced.

Feel free to compare the code and browse around, and let me know your thoughts in the comments section.