Category: Review/overview

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.

Metamath

During my research on various theorem provers, today I stumbled upon Metamath.

To me, what was interesting about it was its simplicity. You start by defining a formal system, i.e. variables, symbols, axioms, inference rules. Then you build new theorems based on the formal system.

The core concept behind Metamath is substitution, and it’s using RPN notation to build hypothesis on the stack and then rewrite them using the inference rules to reach conclusion.

The program is written in C, and I compiled it on both OS X and my Android phone. It’s pretty light-weight and compiles in a few milliseconds, and it’s also interesting that you can take it anywhere you want on your phone.

Metamath has no special syntax. It will tokenize a file that we give to it, and tokens that start with $ are Metamath tokens, while everything else are user-defined tokens.

Here is a list of built-in Metamath tokens:

  • To define constants, use the $c token.
  • To define variables, use the $v token.
  • To define types of variables, use the $f token.
  • To define essential hypothesis, use the $e token.
  • To define axioms, use the $a token.
  • To define proofs, use the $p token.
  • To start proving in $p statement, use the $= token.
  • To end the statements above, use the $. token.
  • To insert comments, use the $( and $) tokens.
  • To define a block (has effect on scoping), use the ${ and $} tokens. Note that only $a and $p tokens will remain outside the scope.

That’s basically it. The package has included demo example and an example for the MU puzzle as well. There are other systems as well (Peano, Set).

There are some basic rules as well:

  • A hypothesis is either a $e or a $f statement
  • For every variable in $e, $a or $p, we must have a $p assertion, i.e. every variable in an essential hypothesis/axiom/proof must have a floating hypothesis (type)
  • A $f, $e, or $d statement is active from the place it occurs until the end of the block it occurs in. A $a or $p statement is active from the place it occurs through the end of the database.

For the complete syntax you can refer to the Metamath book.

Now for the example we’ll use, start by creating a test.mm file. We’ll define a formal system and demonstrate the usage of modus ponens to come up with a new theorem, based on our initial axioms.

$( Declare the constant symbols we will use $)
$c -> ( ) wff |- I J $.

$( Declare the variables we will use $)
$v p q $.

$( Specify properties of the variables, i.e. they are wff formulas $)
wp $f wff p $.
wq $f wff q $.

$( Define "mp", for the modus ponens inference rule $)
${
mp1 $e |- p $.
mp2 $e |- ( p -> q ) $.
mp  $a |- q $.
$}

$( Define our initial axioms. I and J are well-formed formulas,
we have a proof for I and we have conditional for I -> J $)
wI  $a wff I $.
wJ  $a wff J $.
wim $a wff ( p -> q ) $.

$( Prove that we can deduce J from the initial axioms. Note how we use
block scope here, since we don't want the hypothesis proof_I and
proof_I_imp_J to be visible outside of this scope. $)
${
$( Given I and I -> J $)
proof_I $e |- I $.§
proof_I_imp_J $e |- ( I -> J ) $.

$( Prove that we can deduce J $)
proof_J $p |- J $=
wI  $( Stack: [ 'wff I' ] $)
wJ  $( Stack: [ 'wff I', 'wff J' ] $)

$( Note that we had to specify wff for I and J before using mp,
since the types have to match, as set on line 8 and 9 $)

proof_I       $( Stack: [ 'wff I', 'wff J', '|- I' ] $)
proof_I_imp_J $( Stack: [ 'wff I', 'wff J', '|- I', '|- ( I -> J )' ] $)

mp  $( Stack: [ '|- J' ] $)
$.
$}

To verify our file, we run ./metamath 'read test.mm' 'verify proof *' exit.

Note how we had to separate wff from |-. Otherwise, if we just used |-, then all well formed formulas would be proven to be true, which doesn’t make much sense.

In addition to this, the reason why we have implication -> and turnstile provable assertion |- is that the former is a wff (i.e. statement in the object language) and works on propositions, while the latter is not a wff but rather a statement in the meta language and works on proofs.

The arrow -> is usually used to denote an “internalization” of the meaning of turnstile, into the object language. This allows us, in some sense (depending on the meaning ascribed to ->) to represent the relationships between hypotheses and conclusions in the object language, whereas without it it becomes difficult to reason about on a higher-order level (e.g. most systems do not allow A, (A |- B) |- B).

For more complete examples, you can check out:

  • logic.mm – where I define a basic logical system that contains definitions for and-elim and and-intro and proves some theorems.
  • peano.mm – where I define successor for natural numbers and prove some theorems about ordering of them.

Due to its minimalistic design, when compared to Coq it has no Calculus of Constructions, Inductive Types, etc.

To conclude, I think it’s a fun program to play with, but since it has no “real” framework, I don’t think it’s as industry ready as Coq.

JavaScript Patterns overview

Chapter 1

Discusses the following types of patterns:

– Design patterns: singleton, factory, decorator
– Coding patterns: js related
– Antipatterns

Maintainable code is one that:

– Is readable
– Is consistent
– Is predictable
– Looks as if it was written by the same person
– Is documented

One of the general rules in the Gang of Four book says, “Prefer object composition to class inheritance.”. This means that if you can create objects out of available pieces you have lying around, this is a much better approach than creating long parent-child inheritance chains and classifications. In JavaScript it’s easy to follow this advice-simply because there are no classes and object composition is what you do anyway.

Antipattern: do not use. right-to-left evaluation

function foo() {
var a = b = 0;
// ...
}

Antipattern: implied global

function sum(x, y) {
result = x + y;  // The rule of thumb is to always declare variables using var
return result;
}

Antipattern: the first alert will say “undefined” because myname is considered declared as a local variable to the function.

myname = "global"; // global variable
function func() {
alert(myname); // "undefined"
var myname = "local";
alert(myname); // "local"
} func();

Antipattern: don’t augment prototypes because Object.prototype.hasOwnProperty doesn’t show prototype defs, only own

if (typeof Object.protoype.myMethod !== "function") {
Object.protoype.myMethod = function () {
// implementation...
};
}

In the following example, eval() can access and modify a variable in its outer scope, whereas Function cannot (also note that using Function or new Function is identical):

(function () {
var local = 1;
eval("local = 3; console.log(local)"); // logs 3
console.log(local); // logs 3 }());
(function () {
var local = 1;
Function("console.log(typeof local);")(); // logs undefined }());

warning: unexpected return value. need return and { to be on the same line. This behavior can cause troubles when a function returns an object literal and the opening brace is on the next line:

function func() {
return
{
name: "Batman"
};
}

For your constructors, you can use upper camel case, as in MyConstructor(), and for function and method names, you can use lower camel case, as in myFunction(), calculateArea() and getFirstName(). And what about variables that are not functions? Developers commonly use lower camel case for variable names, but another good idea is to use all lowercase words delimited by an underscore: for example, first_name, favorite_bands, and old_company_name.

Chapter 2

Don’t use new Object(); – use the simpler and reliable object literal instead (var x = { ... }).

When you invoke the constructor function with new, the following happens inside the function:

1. An empty object is created and referenced by this variable, inheriting the prototype of the function.
2. Properties and methods are added to the object referenced by this.
3. The newly created object referenced by this is returned at the end implicitly (if no other object was returned explicitly).

var Person = function (name) {
// create a new object
// using the object literal
// var this = {}; i.e. Object.create(Person.prototype);

// add properties and methods this.name = name;
this.say = function () {
return "I am " + this.name; };
// return this;
};

var Objectmaker = function () {
// this `name` property will be ignored
// because the constructor
// decides to return another object instead this.name = "This is it";
// creating and returning a new object
var that = {};
that.name = "And that's that";
return that;
};
// test
var o = new Objectmaker();
console.log(o.name); // "And that's that"

As can you see, you have the freedom to return any object in your constructors, as long as it’s an object. Attempting to return something that’s not an object (like a string or a boolean false, for example) will not cause an error but will simply be ignored, and the object referenced by this will be returned instead.

Chapter 3

> var a = function() { }
undefined
> a.name
''
> var a = function a() { }
undefined
> a.name
'a'
>

Chapter 4

Dependencies, this has faster resolution

var event = YAHOO.util.Event, dom = YAHOO.util.Dom;

The solution to this unexpected behavior is to be careful not to pass references to objects and arrays you want to keep private. One way to achieve this is to have getSpecs() return a new object containing only some of the data that could be interesting to the consumer of the object. This is also known as Principle of Least Authority (POLA), which states that you should never give more than needed. In this case, if the consumer of Gadget is interested whether the gadget fits a certain box, it needs only the dimensions. So instead of giving out everything, you can create getDimensions(), which returns a new object containing only width and height. You may not need to implement getSpecs() at all.

Another approach, when you need to pass all the data, is to create a copy of the specs object, using a general-purpose object-cloning function. The next chapter offers two such functions-one is called extend() and does a shallow copy of the given object (copies only the top-level parameters). The other one is called extendDeep(), which does a deep copy, recursively copying all properties and their nested properties.

var myobj = (function () { // private members
var name = "my, oh my";
// implement the public part return {
getName: function () {
return name; }
}; }());
myobj.getName(); // "my, oh my"

This example is also the bare bones of what is known as “module pattern,” which we examine in just a bit.

One drawback of the private members when used with constructors is that they are recreated every time the constructor is invoked to create a new object. This is actually a problem with any members you add to this inside of constructors. To avoid the duplication of effort and save memory, you can add common properties and methods to the prototype property of the constructor. This way the common parts are shared among all the instances created with the same constructor.

Gadget.prototype = (function () { // private member
var browser = "Mobile Webkit"; // public prototype members return {
getBrowser: function () {
return browser; }
}; }());

The module pattern is a combination of several patterns described so far in the book, namely:

– Namespaces
– Immediate functions
– Private and privileged members
– Declaring dependencies

var x = function(arg) {
if (!(this instanceof x)) {
console.log('Not a singleton, using constructor `' + arg + '`');
return new x(arg);
}
this.moo = arg;
}
var myobj1 = new x('using new');
var myobj2 = x('without new');
console.log(myobj1);
console.log(myobj2);

// constructor
var Gadget = function () {};
// a static method
Gadget.isShiny = function () { return "you bet"; };
// a normal method added to the prototype
Gadget.prototype.setPrice = function (price) { this.price = price; };
The static isShiny() is invoked directly on the constructor, whereas the regular method needs an instance:
// calling a static method
Gadget.isShiny(); // "you bet"
// creating an instance and calling a method
var iphone = new Gadget(); iphone.setPrice(500);

Sometimes it could be convenient to have the static methods working with an instance too. This is easy to achieve by simply adding a new method to the prototype, which serves as a facade pointing to the original static method:

Gadget.prototype.isShiny = Gadget.isShiny;
iphone.isShiny(); // "you bet"

In such cases you need to be careful if you use this inside the static method. When you do Gadget.isShiny() then this inside isShiny() will refer to the Gadget constructor function. If you do iphone.isShiny() then this will point to iphone.

var Gadget = (function () {
// static variable/property
var counter = 0;
// returning the new implementation // of the constructor
return function () { console.log(counter += 1); };
}()); // execute immediately

Chapter 5

Classical Pattern #1-The Default Pattern (prototype chain inheritance)

function inherit(C, P) {
C.prototype = new P();
}
var x = function() {}
var y = function() {}
y.prototype.a = b;
inherit(x, y);

lookup: x -> y -> y.prototype. Object #3 doesn’t have such a method, so it looks up to #2 via the prototype chain. Object #2 doesn’t have it either, so it follows the chain up to #1, which does happen to have it. One drawback of this pattern is that you inherit both own properties added to this and prototype properties. Most of the time you don’t want the own properties, because they are likely to be specific to one instance and not reusable.

Classical Pattern #2-Rent-a-Constructor

function Child(a, c, b, d) {
Parent.apply(this, arguments);
}

This way you can only inherit properties added to this inside the parent constructor. You don’t inherit members that were added to the prototype. But nothing from the prototype gets inherited.

Classical Pattern #3-Rent and Set Prototype

function Child(a, c, b, d) {
Parent.apply(this, arguments);
}
Child.prototype = new Parent();

A drawback is that the parent constructor is called twice, so it could be inefficient. At the end, the own properties (such as name in our case) get inherited twice.

Classical Pattern #4-Share the Prototype

Unlike the previous classical inheritance pattern, which required two calls to the parent constructor, the next pattern doesn’t involve calling the parent constructor at all. The rule of thumb was that reusable members should go to the prototype and not this. Therefore for inheritance purposes, anything worth inheriting should be in the prototype. So you can just set the child’s prototype to be the same as the parent’s prototype:

function inherit(C, P) {
C.prototype = P.prototype;
}

However if one child or grandchild somewhere down the inheritance chain modifies the prototype, it affects all parents and grandparents.

Classical Pattern #5-A Temporary Constructor

The next pattern solves the same-prototype problem by breaking the direct link between parent’s and child’s prototype while at the same time benefiting from the prototype chain. This pattern has a behaviour slightly different from the default pattern (classical pattern #1) because here the child only inherits properties of the prototype.

function inherit(C, P) {
var F = function () {};
F.prototype = P.prototype;
C.prototype = new F();
C.uber = P.prototype; // Store the super class
C.prototype.constructor = C; // If you don't reset the pointer to the constructor, then all children objects will report that Parent() was their constructor
}

A common optimization of the Holy Grail pattern is to avoid creating the temporary (proxy) constructor every time you need inheritance.

var inherit = (function () {
var F = function () {};
return function (C, P) {
F.prototype = P.prototype;
C.prototype = new F();
C.uber = P.prototype;
C.prototype.constructor = C;
}
}());

function f() {
var args = [].slice.call(arguments, 1, 3);
return args;
}
// example
f(1, 2, 3, 4, 5, 6); // returns [2,3]

function bind(o, m) {
return function () {
return m.apply(o, [].slice.call(arguments));
};
}

Chapter 6

function Universe() {
// do we have an existing instance?
if (typeof Universe.instance === "object") {
return Universe.instance;
}
// proceed as normal
this.start_time = 0; this.bang = "Big";
// cache
Universe.instance = this;
// implicit return:
return this;
}

Another way to do the class-like singleton is to use a closure to protect the single instance. You can implement this by using the private static member pattern discussed in Chapter 5. The secret sauce here is to rewrite the constructor:

function Universe() {
// the cached instance
var instance = this;
// proceed as normal
this.start_time = 0; this.bang = "Big";
// rewrite the constructor
Universe = function () {
return instance;
};
}

Patterns

Singleton

Creating only one object of a “class.” We looked at several approaches if you want to substitute the idea of a class with a constructor function and preserve the Java-like syntax. Otherwise, technically all objects in JavaScript are singletons. And also sometimes developers would say “singleton,” meaning objects created with the module pattern.

Factory

A method that creates objects of type specified as a string at runtime.

Iterator

Providing an API to loop over and navigate around a complex custom data structure.

Decorator

Tweaking objects at runtime by adding functionality from predefined decorator objects.

Strategy

Keeping the same interface while selecting the best strategy to handle the specific task (context).

Facade

Providing a more convenient API by wrapping common (or poorly designed) methods into a new one.

Proxy

Wrapping an object to control the access to it, with the goal of avoiding expensive operations by either grouping them together or performing them only when really necessary.

Mediator

Promoting loose coupling by having your objects not “talk” to each other directly but only though a mediator object.

Observer

Loose coupling by creating “observable” objects that notify all their observers when an interesting event occurs (also called subscriber/publisher or “custom events”).