Testing, Simulation, and Formal Methods

Testing, simulation, and formal methods are three common techniques in verification. However, distinguishment between them is not very clear to many people working in other CS disciplines. I found two examples in Wang Farn's slides very helpful in explaining their differences──the three techniques are visualized by three correspondent approaches to answer the following two questions.

Q: Do the 3 angles in every triangle sum to 180 ?

Testing (check all triangles you see)

• Expensive 
• Low coverage
• Late in development cycles

Simulation (check all triangles you draw)

• Economic 
• Low coverage
• Don't know what you haven't seen

Formal Verification (prove it)

• Expensive
• 100% coverage
• Proofs may be automatically verified

Q: What is the robustness of a new design of call?

• Testing (let real cars hit a real wall)
• Simulation (let virtual cars hit a virtual wall)
• Formal Verification (verify the car models)

Wang Yin also wrote a blog article trying to explain the difference between testing and static analysis (one of the popular formal methods) in plain words.

The OOP Enssences in JavaScript

Instantization

// The following code shows how Firefox implements the "new" operator
function Point(x, y){ 
    this.x = x; this.y = y;
}
function ObjectFactory(){
    var obj = {};
    var Constructor = Array.prototype.shift.call( arguments );
    if(typeof Constructor.prototype === 'number')
        obj.__proto__ =  Object.prototype;
    else
        obj.__proto__ =  Constructor.prototype;
    var ret = Constructor.apply(obj, arguments);
    return typeof ret === 'object' ? ret : obj;
}

// This is equivalent to: var p = new Point(0, 0);
var p = ObjectFactory(Point, 0, 0);

Inheritance

// The following code is generated by CoffeeScript to 
// implement subclass inheritance
var __extends = function(child, parent) {
    for (var key in parent) {
      if (Object.prototype.hasOwnProperty.call(parent, key)) {
        child[key] = parent[key];
      }
    }
    function ctor() { this.constructor = child; }
    ctor.prototype = parent.prototype;
    child.prototype = new ctor;
    child.__super__ = parent.prototype;
    return child;
};

// Our code
var Person = function(name) {
    console.log('Hi, I am ' + name + '!'); 
    this.name = function(){ return name };
};
var Student = function() {
    Student.__super__.constructor.apply(this, arguments);
};
__extends(Student, Person);    // make Student a subclass of Person
var me = new Student('Eric');  // "Hi, I am Eric!"
console.log(me.name());        // "Eric"

Seeded PRNG in JavaScript

Below is a multiply-with-carry (MWC) random generator with a pretty long period, adapted from wikipedia Random Number Generators:

// Takes any integer
Math.seed = function(s) {
    var m_w = s;
    var m_z = 987654321;
    var mask = 0xffffffff;
    return function() 
    // Returns number between 0 (inclusive) and 1.0 (exclusive),
    // just like Math.random().
    {
        m_z = (36969 * (m_z & 65535) + (m_z >> 16)) & mask;
        m_w = (18000 * (m_w & 65535) + (m_w >> 16)) & mask;
        var result = ((m_z << 16) + m_w) & mask;
        result /= 4294967296;
        return result + 0.5;
    }
}

Another fast and simple PRNG, without magic numbers:

Math.seed = function(s) {
    return function() {
        s = Math.sin(s) * 10000;
        return s - Math.floor(s);
    };
};

You can replace the default PRNG of JavaScript by, e.g.,

Math.random = Math.seed(Math.round(Math.seed(42)*10000));

Reference

1. http://stackoverflow.com/questions/521295/javascript-random-seeds/521323
2. https://github.com/davidbau/seedrandom

Lo-Dash v.s. Underscore

A breakdown of the advantages of Lo-Dash over Underscore:
http://kitcambridge.be/blog/say-hello-to-lo-dash/

The creator of Lo-Dash explain why it is a superior choice to Underscore:
http://stackoverflow.com/questions/13789618/differences-between-lodash-and-underscore

Lo-Dash v.s. Underscore benchmarks: http://jsperf.com/lodash-underscore

One may wonder that, since Lo-Dash is intended to be a superset compatible to Underscore from the beginning of design, why not contribute to Underscore directly, e.g. by merging the new features back into Underscore, instead of developing a new library? This thread in GitHub may serve as an answer to the question.

Reset MySQL slave when it is out of sync

2019/01/24:
Fix bin-log when the log files are missing:
https://www.redips.net/mysql/replication-slave-relay-log-corrupted/

Slave side:

# stop all slaves before resetting the master
(mysql) STOP SLAVE;

Master side:

# set the master database to read-only
(mysql) FLUSH TABLES WITH READ LOCK;

# backup the current database
(bash) mysqldump -u root -p -databases db1 db2 | bzip2 > /tmp/bak.sql.bz

# reset the binary logs
(mysql) RESET MASTER;

Slave side:

(bash) scp -r ericpony@XXX.XXX.XXX.XXX:/tmp/bak.sql.bz /tmp

# load the current database from master
(mysql) SOURCE /tmp/bak.sql.bz;

# reset the binary logs
(mysql) RESET SLAVE;

# restart slave
(mysql) START SLAVE;

Master side:

# unlock the master database
(mysql) UNLOCK TABLES;

Slave side:

# check if everything is ok
(mysql) SHOW SLAVE STATUS \G

Reference

http://www.cnblogs.com/sunyuxun/archive/2012/09/13/2683338.html

Install Node.js on Ubuntu

Using Launchpad repo by Chris Lea just run following commands:

apt-get install python-software-properties
apt-add-repository ppa:chris-lea/node.js
apt-get update

apt-get install nodejs npm

Clojure resources

Learning category theory in Clojure:  http://www.clojure.net/archive.html