Decision Procedures for Presburger Arithmetic

Note: This post will be edited as I learn more.

One of the results of Gödel's Incompleteness Theorem is that deciding the validity of arbitrary mathematical formulas is impossible. Here, deciding the validity means telling if "1 < 2" is true or false. Of course, the impossibility result is for arbitrary mathematical formulas and not for simple equalities and inequalities. If we could somehow restrict ourselves to simple formulas (which arise in practice), we might get a complete decision procedure.

Presburger Arithmetic is a first-order theory of natural numbers with addition. Though it doesn't support division amongst other things, it's of interest because it is decidable. Again, decidability means that we can build machines (or algorithms - doesn't make any difference) which, given a Presburger formula, correctly return "true" or "false" but never say "don't know".

Michael Norrish of ANU gives an overview of two such algorithms: Fourier-Motzkin Variable Elimination and Omega Test. John Harrison of Intel has provided a library of OCaml functions for automated theorem proving, which includes Cooper's algorithm.

I'll briefly cover how to use John Harrison's library and Omega Test as part of your system. My interest is in checking if a list of linear constraints has a solution or not. As an example, we'll see how to use these libraries to check

exists y. y > 2 && y < 50;

John Harrison's OCaml Library

You need OCaml to interactively run or build an executable of this library. Unzip and un-tar the archive and build using "make." Once you have done that, you can run a set of examples by running "./example" built by the make process.

The .ml files in the package are dependent on each other. It's not easy to take a fragment out of it and compile that separately (unless you are a good Caml programmer). But you don't need to take out the needed fragments, either. You can make your own example file (example.ml) and re-build using "make." In my case, I changed example.ml to:

open Atp;;
open Format;;

let print_formula fm = formula_printer print_atom fm; print_newline();;
let result = integer_qelim << exists x. x > 2 /\ x < 50 >> in
print_formula result

If I run "./example" I get <<true>> at the console. Unfortunately, no documentation is available but there are several examples in the .ml files that can give you insight into how to use it.

There are several ways to integrate it with your software. The ugliest one is to write an example.ml that reads formulas from a text file (generated by your software) and invokes integer_qelim on it. The result can be written back to an output file. If you are using Java, you might be interested in CamlJava which provides an interface between Java and Caml using JNI and extern. I might try that out and post my experience.

Omega Test

I could compile Omega only with gcc 2.95 on a Solaris box. The later versions of gcc give errors. The project also seems to be abandoned but it's widely quoted at different places. You can get release 1.2 from here. Follow the following steps to compile:

make depend
make libomega.a
make libuniform.a
make libcode_gen.a
make oc

Omega works on sets and relations. The compiled executable (called Omega Calculator) can be found in omega/omega_calc/obj. It's built on top of Omega Library. Instead of using the calculator, you can invoke the library from your code as well, as this interface document explains.

I created a test.txt file with the following contents:

S := {[i] : i <= 50};
T := {[j] : j >= 20};

S intersection T;

And I could run the calculator on this file ("./oc test.txt") and get the following output:

Omega Calculator v1.2 (based on Omega Library 1.2, August, 2000):
# S := {[i] : i <= 50};
#
# T := {[j] : j >= 20};
#
# S intersection T;

{[In_1]: 20 <= In_1 <= 50}

As you can see the constraints have been combined. If they were unsatisfiable (such as contradictory constraints) you would have gotten:

Omega Calculator v1.2 (based on Omega Library 1.2, August, 2000):
# S := {[i] : i >= 50};
#
# T := {[j] : j <= 20};
#
# S intersection T;

{[In_1]: FALSE}

I hope there is a way of getting a "witness" back from these decision procedures.

Installing Java Path Finder (JPF) on Linux

[This has been written because as of now, JPF doesn't compile and work without giving you some trouble, and it took me quite some time to resolve the issues. Things might have improved at the time you read this. Also, I have tested it only on Gentoo Linux (please let me know if it breaks on a particular Linux distribution; I know there are more problems with installation on other *nix, particularly Sun Solaris)].

First things first: JPF doesn't work with Java 1.5 (aka 5.0) because of its dependence on BCEL library. If you have been able to compile successfully but can't execute JPF on simple examples (does it hang for ever?), most probably, your java version is not compatible with BCEL. Unfortunately, you will have to install an older version of JDK, perhaps 1.4.2.

Secondly, You must have JAVA_HOME variable set to your jdk root and javac should be in the PATH environment variable.

1. Checking out the source code

Create a folder where you want to download JPF. Change your working directory to that folder and type the following as a single command:

cvs -d:pserver:anonymous@cvs.sourceforge.net:/cvsroot/javapathfinder co -P javapathfinder

2. Check if you have ant installed

If you are using a new Linux distribution, most probably you already have it. Don't download in that case.

ant -version

If it displays you the version number of ant, you can read ahead. Otherwise, download and install ant first.

3. Download the "convenience libs"

JPF needs a few jars to work properly, namely BCEL, Xerces and a particular MD5 library. The JPF team has put them in a single zip (though they are older versions but they are known to work). You can download them as jpf-lib.zip from here. For convenience, move the zip file to the javapathfinder folder and unzip using the following command:

unzip jpf-lib.zip

This will create a lib folder and place the needed files there.

4. Compiling

If you now do "ant -projecthelp" from within javapathfinder folder, it will display different build options. You can build the core (without the JUnit tests) by invoking

ant compile

5. Testing out the software

(a) HelloWorld

cd examples
javac HelloWorld.java
../bin/jpf HelloWorld

It should print "Hello World!" with a thread stack trace and a "No Errors Found" message.

(b) AssertionCheck (assuming you are in the javapathfinder/examples folders)

javac AssertionCheck.java
../bin/jpf AssertionCheck

It should show you the exception trace.

6. Writing Your Own Example

If everything is working perfectly till this point, you are done. You can read the source code of the two simple examples given above. A slightly more complicated example that I tried with JPF is given below:

Suppose, we have written a findMax() function with a bug that it starts searching for the maximum value in an array starting at index 1. First, of all we have to write a "test driver" and state the properties that we expect from the code. This is given below in main(). We initialize the array with random values from Verify class.

import gov.nasa.jpf.jvm.Verify;

public class MaxWhile {
   public static int findMax (int []a) {
       int k = 1;
       int max = a[1];

       while (k < a.length) {
           if (a[k] > max) max = a[k];
           k++;
       }

       return max;
   }

   public static void main (String args[]) {
       int [] myArray = new int [Verify.random(10)];
       if (myArray.length <= 1) return;

       for (int i=0; i<myArray.length; i++)
           myArray [i] = Verify.random(10);

       int max = findMax (myArray);
       for (int i=0; i<myArray.length; i++)
           assert (max >= myArray[i]);
   }
}

Save as MaxWhile.java in examples folder. This can be compiled with javac by having gov.nasa.jpf.jvm.Verify in classpath.

javac -cp ../build/jpf MaxWhile.java
../bin/jpf MaxWhile

The code initializes an array of a random size (upper limit 10) with random values. It then finds the maximum value and checks that the maximum value obtained is indeed greater than or equal to any other value in the array. The error trace generated by JPF has Random#i at different points which collectively comprise the counterexample. They tell you different values for the random numbers that cause your assertion to fail.

Proving Loops with Loop Invariants

In continuation to the proof obligation posted last week, I decided to explore loop invariants. This means converting the for loop in the code to a while one. The new proof obligation is as follows:

\problem {
\<{ int[] a; int max; }\>
(
 (!a = null & a.length > 0) ->
 (
  \<{ 
   max = a[0];
   int k = 1;
   while (k < a.length) {
    if (a[k] > max) max = a[k];
    k++;
   }
  }\>
  \forall int i; (i < a.length & i >= 0 -> max >= a[i] )
 )
)
}

Now, this is much easier to prove if we can select a proper loop invariant. What is it that holds before the loop starts execution, remains true after each iteration and holds even after the loop termination? A good first attempt can be

\forall int i; (i >= 0 & i < k -> max >= a[i])

Again, the syntax is specific to KeY but the semantics are valid for any theorem prover for imperative languages. A stronger invariant can be more useful and in fact, in this particular example, the loop invariant can be strengthened to

k > 0 & k <= a.length & 
\forall int i; (i >= 0 & i < k -> max >= a[i])

There are two subcases (amongst others) generated by KeY when a loop invariant is used: Invariant Initially Valid and Body Preserves Invariant. Since we are dealing with necessity (signified by <code in angle brackets>), and not with just a possibility, we have to show termination of the loop as well. In other words, we have to show that the loop terminates and, after termination, the formula holds. Thus, the third case to prove is Termination.

Invariant Initially Valid:
 a.length >  0
==>
 \forall int i;  (i >= 0 & i <  1 -> a[0] >= a[i])


Body Preserves Invariant:
   _k >  0
 & _k <= a.length
 & \forall int i; 
     (i >= 0 & i <  _k -> _max >= a[i]),
 a.length >  0
==>
 {
   k:=_k,
   max:=_max}
   \[{method-frame(()): {
             if (k < a.length) {
                if (a[k] > max)
                   max=a[k];
                k++;
             }
       }
     }\] (\forall int i; (i >= 0 & i <  a.length -> max >= a[i])
  }

But termination is not easy to show unless we can somehow tell that something is gradually approaching towards a limit which will make the while statement false. This is where the concept of Variant is Decreasing comes in. In KeY, we can define that a.length - k is decreasing with each iteration of the loop. With the help of this statement (which of course, we have to prove separately), Termination subgoal takes the following form:

(a.length - _k) <= 0
==>
 {k:=_k,
  max:=_max}
  \<{
      while ( k < a.length ) {
         if (a[k]>max)
           max=a[k];
         k++;
      }
  }\> true

This is, of course, very easy to prove because of the premises of the implication; the loop will not execute at all and there is no statement after the loop, Hence, the termination. But while doing this, we have introduced a new sub goal: Variant is Decreasing. We have to prove that with each iteration of the loop a.length - k is actually decreasing. This subgoal has the following form:

 _k_1 >  0,
 _k_1 <= a.length,
 \forall int i;  (i >= 0 & i <  _k_1 -> _max_1 >= a[i]),
 {k:=_k_1}
   \<{method-frame(()): {
         var=k       }
     }\> var = TRUE,
 a.length >  0
==>
 {k:=_k_1,
   max:=_max_1,
   var_1:=a.length - _k_1}
   \<{
        if (a[k]>max)
          max=a[k];
        k++;
     }\> (a.length - k) <  var_1

It looks daunting but after symbolic execution of the code, it's pretty simple.

Once we have proved everything regarding the invariant, we can use the invariant to prove the real thing, which was the following first order logical formula:

\forall int i; (i < a.length & i >= 0 -> max >= a[i] )

Thus, the fourth case, called Use Case is something of the form

k > 0 & k <= a.length & 
\forall int i; (i >= 0 & i < k -> max >= a[i]) ==>
\forall int i; (i < a.length & i >= 0 -> max >= a[i] )

which is much easier to prove than the standalone formula that we initially had.

---

My affair with loop invariants was a very short one. Perhaps, I'll come back to these in future. At present, I'm moving on to manually injecting bugs in this code and trying to find them using KeY.

First Steps in Theorem Proving using KeY

Now something very technical! I'll try to keep it simple; as simple as possible, but not any simpler.

Following is a .key file that has Java code in between \<{ and }\>. The code looks for the maximum element in the array. The first order logical formula (after the block of code) says that when the code has been executed, the variable max will hold a value greater than or equal to every element of the array.

\problem {
\<{ int[] a; int max; }\>
(
 (!a = null & a.length > 0) ->
 (
  \<{ 
   max = a[0];
   for (int i=0; i<a.length; i++) {
    if (a[i] > max) max = a[i];
   }
  }\>
  \forall int i; (i < a.length & i >= 0 -> max >= a[i] )
 )
)
}

This format is internal to the KeY tool. But the ideas will be similar to any theorem prover for imperative programming languages, like Java.

At the moment, I am stuck up because there is no upper limit on the size of the array, which tells me that the only way to prove the formula is to use induction. Now, the only sequence that can be made a basis for induction is the size of the array. I'm trying to figure out how to state this in KeY.

A Theorem

Theorem: Consider the set of all sets that have never been considered.

Hey! They're all gone!! Oh, well, never mind...


(Reference)

Java Memory Model (Fixes in J2SE 5.0)

[This is inspired from Erik Poll's talk in the 4th KeY symposium.]

Immutable Objects are of interest for software verification because they are easy to argument about in presence of concurrency. Verification of concurrent programs is much harder than sequential ones because threads can effect shared variables in subtle ways. However, if an object is immutable, we don't need to think that different threads will see inconsistent values.

An example of an immutable class is Integer: you can't modify the value of Integer once it has been created. Other examples where immutability makes sense are classes for representing URL's, Date, Property Files, etc.

Suppose you are writing an immutable class MyInteger as follows:

public class MyInteger {
   private final int i;
   public MyInteger (int value) {
      i = value;
   }
   public int getValue () {
      return i;
   }
}

This class is immutable because all the members are private (as well as final) and there is no setValue() method in the class. The client code can give the instantiating value but can't modify it later. Assume a client uses the class as follows:

x = new MyInteger (5);

If another thread tries to access the shared variable x, we would expect x.getValue() to give 5 (or throw a null pointer exception, but not 0 in any case). However, the Java Language Specification didn't ensure that! The default initialization value of an integer is 0 and it's later changed to 5! Following the old spec, it's possible that running on a particular JVM, a thread would get 0 and later 5 for x.getValue().

With JSR 133, which has been officially implemented in J2SE 1.5 aka 5.0, this has been fixed by giving formal mathematical semantics to Java Memory Model as well as doing some formal proof for some desirable properties.


This has very profound conclusions:

Firstly, software is complex. How can you explain to your customer that the code that worked perfectly in thousands of test runs failed right during the demo?

Secondly, it means that as a software developer, you should restrict yourself to only a single set of tools as it's impossible to be master of all. Moreover, you need to keep yourself abreast of the activity going on related to that tool. Read JSRs, participate in online discussions, etc.

Thirdly, and most importantly, it proves once again that one should have a formal Mathematical semantics of programming languages as well as some formal proofs of correctness - at least of something as significant as Java itself. Moreover, we need more and more peer review to write better software. This indirectly supports the Open Source Initiative.

This article at java.net is a must read if you can spare some time.

The KeY Project

[This is being written as an informal introduction to the KeY tool for software developers who don't have background in Logic and Automated Theorem Proving. If you are interested in theoretical aspects, consider reading from the list of research papers from people working on the project.]

The most common way of testing software in the industry is to pass it on to the QA team after development. Depending on the expertise of the QA personnel, they may come up with scenarios where the software doesn't "behave" as per the "expectations." If your company is somewhat sophisticated, writing these "expectations" in the form of functional specifications might be part of the software development life cycle. If you are even more sophisticated (or the correctness of your software is critical), you might even write pre- and post-conditions with each function/ method in your software.

As part of UML, OMG also defined Object Constraint Language (OCL). With OCL, for example, you can write class invariants (statements that always remain true for every instance of a class) and pre- and/ or post conditions for each method. With these things in place, an obvious need arises for checking whether the code satisfies these constraints or not.

The KeY tool (a joint project of the University of Karlsruhe, Chalmers University of Technology and the University of Koblenz) seamlessly integrates with Borland's Together Control Center (now called just Together) - a UML modeling solution. [Work has been done for JML support with Eclipse as well.] One of the features of Together, for example, is that it let's you draw UML diagrams for which it generates skeleton code. OCL expressions are written as comments in the code (somewhat similar in fashion to javadocs). The KeY tool can be used to verify the code against these constraints. It empowers you to find errors within the constraints as well.

As a very simple (and somewhat stupid) example consider a class Account with an attribute balance and two methods deposit () and withdraw (). Let's compare the following two implementations of withdraw() against the class invariant balance >= 0:

public boolean withdraw (int amount) {
   balance -= amount;
   return true;
}

public boolean withdraw (int amount) {
   if (balance < amount)
      return false;

   balance -= amount;
   return true;
}

The implementation on the top is said to break the class invariant, while the one below "preserves" it. An attempt to prove the correctness of the code on the left will fail. While an automated theorem prover might not be needed for complete verification of the applications in the industry, there are specific areas where 100% verification is a need: for example, in safety critical application; or in case of smart card applications where it's almost impossible to recollect all the smart cards from the customers in case a bug is later detected. The latter of the two areas is the main focus of KeY.

Amongst other things, the KeY tool can check your implementation as well as specifications for structural subtyping, behavioural subtyping, satisfaction of post conditions on method invocation and preservation of class invariants. For a not-so-obvious-at-first-sight example, consider the following invariant alongw ith the code that follows:

//Note: these are not 100% accurate OCL expressions
pre-condition: i >= 0 and j >= 0 and
         i<arr->size and j<arr->size
post-condition: arr[i] = arr[j]@pre and arr[j] = arr[i]@pre
void swap (int arr[], int i, int j) {
   arr[i] += arr[j];
   arr[j] = arr[i] - arr[j];
   arr[i] -= arr[j];
}

The code swaps two elements in an array by using integer arithmetic (and avoids use of a temporary variable). However, it violates the specs when you invoke it with i=j. Such non-obvious cases may be missed by the QA people as well. Unfortunately, testing can only show the existence of bugs but not their non-existence. The only guaranteed way of "proving" program correctness is either to use a theorem prover, like KeY, or to exhaustively test every possibility.

---

Philipp Ruemmer has written a paper on this topic. I shall be extending the work (hopefully) for generating counter examples. I'll also get the opportunity to attend the 4th KeY Symposium from 8th to 10th of June.

Lambda Calculus and Mathematical Foundations of Programming Languages

[This has been written as informal introduction to Lambda Calculus. If you are a student of Programming Languages, consider a formal introduction instead. Beyond the second para, this post may not be suitable for kids. Rating: PG13.]

Turing Machine is a well known concept in computer science. It's an abstract machine, capable of implementing any computable function. It's impressive because the machine itself is extremely simple, having only a few instructions. But Turing Machine is more like hardware (a machine) and less like a programming language.

Lambda Calculus is a similar concept (that is, you can define any computable function in it) proposed by Alonzo Church in 1930. The difference form Turing Machine is that it is a programming language; an extremely simple one. There are only two constructs: function definition and function application. The functions themselves are anonymous (i.e., no names are given to functions) but the parameters are named.

Since nothing exists other than these two constructs, everything is represented as a function, even natural numbers. For example, the number 0 can be a function that takes a parameter (actually another function) and returns it. The number 1 can be represented by a function that takes a function and applies the given function to a parameter once. The function for the number 2 can apply the given function to the result of applying the same function to an argument. Obviously, the results of computations are also functions.

[Sideline: Though this definition of natural numbers may seem weird but what exactly is a number, say 1? 1 is something which is different from 0 and 2 (and other numbers as well). There is no other definition. I tried to do a search on this claim of mine and found this excellent piece of argument: What is a number? that quotes Bertrand Russell as, "A number is the class of all classes similar to a given class."]


As you can probably guess, much of the power of Lambda Calculus comes from recursion and our ability to think abstractly. Why is lambda calculus important? Firstly, it is extremely mathematical in nature (why is that a desirable property is discussed next). Secondly, it has resulted in the development of functional programming languages like Lisp, ML, Scheme and later Haskell. Why functional programming is important isn't discussed here (see, Von Neumann Bottleneck, a term coined by John Backus in his Turing award lecture in favor of Functional Programming.)

So I said that Mathematical basis is an important property of any programming language. When we think of something, our thought is unbounded. But when we say the same thing, we have to filter out ambiguity and inconsistency from our thought. Next, when we write the same thing, we have to follow some rules of grammar and (due non-interactive nature of discussion and also because of lack of body language) we have to be even more prcise. Inspite of that, natural language is ambiguous. Consider this sentence, "I can't dance." Does this mean you can't dance now or does it mean that you don't know how to dance?

Mathematics is the most precise language we know to describe things. Programming languages that have foundations in Mathematics are more precise and more importantly, we can argue about their properties formally (e.g., we could try to prove that a given program always terminates). Proving properties of non-formal languages is an extremely daunting task.


You can read more about Lambda Calculus and Formal Semantics of Programming Languages, both on Wikipedia. But don't overdo it - if you are a regular programmer, it's important to know that these things are there; learn and use them when you need them. Hopefully never :)

Ensemble

Group Communication is a complex topic. If you ask software developers about it, they will say that it's just making two entities communicate and thus, isn't more difficult than deciding upon a protocol and writing the code. But solid group communication is hard to build and there is considerable theory involved. Take example of a serious chat application where the order of messages as well as failure to receive them is to be taken care of.

First of all, in the presence of message lost, you face the Two Generals' Problem, which says that it's impossible to achieve agreement on a message if arbitrary number of messages can be lost. In the presence of message lost, if you send an acknowledgment for guaranteeing message delivery, the acknowledgement itself may get lost and thus you need to acknowledge the acknowledgement. But then this will continue forever. Thus, Two Generals' Problem is not solvable. You can read in detail here.

Next, in order to achieve fault tolerance, you have to consider Byzantine Faults which are based on Byzantine Generals' Problem (why distributed systems people always think of army and generals is beyond me). Byzantine Faults occur when a faulty node says different things to different nodes - it may say that I have received the message successfully to one node and report the opposite to some other node, causing confusion and inconsistency in the system. Unlike the Two Generals' problem, it's solvable but with some upper bounds on the number of faulty nodes and with lots of communication overhead.

So, we ignore fault tolerance for now. Consider, ordering of messages instead. In a serious chat application the ordering can matter a lot. If different members in a conversation get messages in different order, it can cause confusion. TCP/IP provides ordering within packets of a single message (where packets are formed at lower layers of the network protocol) that is sent via a single TCP/IP socket. But what about different sockets (different members in the conversation) or different messages sent on the same socket? There is nothing in TCP/IP which guarantees that when you send "Hello"; close the socket; open it again and then send "Goodbye", they will be received in the same order. So, what's the solution? Number the messages yourself! And on the receiving end, hold messages if they are received earlier than their predecessors.

Then comes the issue of Group Membership. Does your rock-solid chat application allow a member to join in between a conversation? If yes, what happens when somebody has sent a message but it hasn't been received by all yet, and a new member joins the group. Should he be delivered the message or should it be held back? If you deliver the message to him as well, some of the members (who received the message before the new member joined) will think that he didn't get that message, while others will think the opposite. More confusion and inconsistency.

Some of you might think that considering all these issues is an overkill for a chat application. What about a distributed group of servers trying to synchronize their end-of-day activity?


As I said in the beginning, there is more to group communication than we casually think of. Ensemble is a library written in Objective Caml that handles most of the theoretical issues involved with Group Communication. It provides simple to use api for Java, C, C# and ML. It's highly modular and reconfigurable. Do check out the features it provides if you are interested in group communication. You can get an idea of the research involved with this library by looking at the list of publications.

Formal Methods for Software in the Industry

A few days back, Byron Cook, from Microsoft Cambridge came to give a guest lecture in the Formal Methods course. The guy, if you could call him that, talked about SLAM which Microsoft is now using internally for proving correctness of device drivers.

Amongst other things, he showed how, by using their software, the developers of Parallel Port device driver found two invocations of an IO completion API in a particular scenario. He said that a lot of Program Managers within Microsoft have started showing interest in Mathematical Logic and Formal Methods after Bill Gates personally congratulated the team. ;)

Other than increasing my interest further with Formal Methods, he talked about his former company, Prover Technology, which means that people are now building commercial products out of Formal Methods.

The lecture was quite complex keeping in view that we have just started studying this field of computer science. And this is one of the most complex fields within computer science; perhaps, as complex as Analysis of Algorithms. What I have learned uptil now starts from Propositional Logic and ends at First Order Logic. The lectures in this course will also cover Dynamic Logic but I still feel that we know nothing.

I have finally made up my mind to do thesis in formal methods and I have a few more months to start that. Fortunately or unfortunately, the Disrtributed Computing Research Group within Chalmers is not so active.

Minesweeper is NP-Complete

Surprising but it's true that Minesweeper is NP Complete. If you remember the definitions from your Algorithms/ Complexity Theory course, to prove that a problem X is NP-Complete you need to reduce a well-known NP-Complete problem (usually satisfiability problem) to X in polynomial time. Solving any NP-Complete problem in polynomial time means that all Non Polynomial time problems would be solved.

And if you can't recall what NP was, let me remind you that problems which require exhaustive analysis of all possibilities to find the best solution are Non Polynomial time. And if you are as dumb as me you will need an example to understand this: Suppose you want to check if a string A is a substring of B and assume that the only possible method is to generate all possible substrings of B and match A against each one of them, then string matching would have been an NP problem.

Some Sokoban addicts seem to be interested in proving that their game is even more complex.

With this comes the "Is P=NP?" question. It's one of the Millennium Questions; there is $1 million award for the person who answers it with mathematical precision.

To this day, I fail to comprehend the difference between NP Complete and NP Hard. Also, some problems are said to be NP Complete in the strong sense. Can any enlightened reader shed some light?

---

Today, we have CHARM day at Chalmers. The industry comes to interact with the students. After many days of inactivity, once again, I am starting exercise and better time management from today.

Assignments: Concurrent Programming and Formal Methods

One of the most famous assignments in DCS program at Chalmers is Train Control in the Concurrent Programming course. Apparently, it's a very good way of learning about critical sections and locking. It can also be extended to classical problems such as readers and writers by drawing the tracks in a different way. But the problem with the assignment is that when you apply brakes, the trains don't stop immediately. They slow down gradually and the time they take to come to a halt depends on their speed. Having the goal to run the trains at the maximum possible speed while managing to brake right before entering the critical section makes the assignment hard and, for me, very boring. It took me one day and one whole night at the university to complete it.

Another assignment that took most of the time last week was to simulate an elevator. We had to write it in Lustre. Chalmers has one of the finest teams in the world when it comes to formal methods for software. One of the Associate Professors, Koen Claessen, has hacked Luke that we use instead of the compiler from the authors of Lustre. Luke generates an HTML page from a Lustre file with all propositional logic embedded into it. It's very interesting. Another tool, KeY, also developed at the university, is used for complex automated verification of software properties.

If life and time permits, I intend to introduce some of these courses when I go back to Pakistan.

"Snow is white" is true if and only if snow is white

Tarski was the first person who argumented in this manner. Considering this from a purely software development point of view (and not as a Logician or Mathematician), this corresponds to the difference in the following two statements:

string s = "2+3 > 5";
bool b = 2+3 > 5;

As you can see, the two statements look alike but they are very different. The first one is just a sequence of symbols and the later is actually a comparison. However, one can write an eval function:

bool b = eval (s);

This can be thought of as interpretation of the syntax into semantics.

Trivial as it might seem, many people forget the difference while designing systems and realize this only some time later during development. For example, many times I have heard people saying, "we can store the names of the functions in a database table and call appropriate function by searching the name in the table." This really happens when people are naively designing a workflow engine kind of thing. How on earth are you going to relate the code with the string from the table? You need reflection!

I wanted to say a lot more but while writing this and looking for appropriate links, I found out this pdf. Too bad for me; nowadays, it's hard to come up with stuff people have not already thought of. I was trying to relate the completeness property of logic with software.

---

I just finished my second term here. The exams went pretty well, Alhumdo Lillah. My push-ups count has reached 3,597 in 30 days and I am lagging by 483 now! Exams are to be blamed.

پڑھ پڑھ لکھ لکھ لاویں ڈھیر، ڈھیر کتاباں چار چپھیر
گردے چانن، وچ انھیر، جاندی عمر نہیں اعتبار
اکو الف تیرے درکار

(Bulleh Shah, Sung by Junoon)

Status Update

I have been here in Sweden for more than three and a half months now. About a quarter of the total time has passed. Within a week the final exams for the second quarter will start.

I took two courses -- Computer Security and Mathematical Logic this term.

The first lecture of Mathematical Logic was quite exotic for me; almost as exotic as Discrete Mathematical Structures was for me in the undergraduate days. Now, I can differentiate among Number Theory, Algebraic Structures and Logic. Jan Smith started the course with discussion on Foundations of Mathematics. Quite honestly, I couldn't understand even a single word from the lecture but it was very surprising for me as I believed I already knew Propositional and First-Order Predicate Logic that constituted more than half of the course.

When I came home after the first lecture, I opened up Firefox and started looking for the Foundations of Mathematics. Really, to my surprise whatever Jan Smith had said was available on Wikipedia as well. I have been studying till now, have learned quite a few things and might continue my exploration of the foundation after the exams.

Computer Security, however, is a very dull course. It's an undergraduate level course and I fail to understand why it is a compulsory course for Dependable Computer Systems. There are two sequels to this course: Language Security and Network Security. I think both of them will be very interesting.

Meanwhile, I have once again started reading Quran. I have done this for the fourth time in the last two years. Last time I had reached uptil para number 8. This time, I am noting down ayaats that I don't understand and those that I could understand and use them for reference sometime.

I should be free from exams after 15th. I intend to visit Stockholm. I also want to learn Swedish Language. And I have prepared a reading list for vacations. It's warm again. Yes, now I understand why Swedes call temperature above freezing point as "warm."

My pushups count has reached 2,815 in 21 days and I am lagging by 41 to maintain an average of 136. This has resulted in good effect on arms and specially on chest. But I must combine this with some other exercise, perhaps reach-ups.