nondeterministic . net

Finally took the second-round exam in Formal Specifications for Complex Systems this morning. Thus finally finishing my second semester at the Technion.

There were a decent number of people at the exam, which either means that lots of other folks also skipped the first one, or that the first exam was hard. Either way, I was glad not to be the only one specifying a message-reversing queue in LOTOS, a drawbridge in temporal logic and Statechart, and simplified C++ classes in Z.

I’m a bit disappointed that there was no Larch on the quiz… in Larch you specify systems by defining an algebra over operations and formal variables, avoiding the need to define abstract data representations. For example, you might specify that top(push(S, e)) = e - i.e., calling top on a LIFO stack that just got pushed e gives you e. Never mind how the stack stores the e, as long as it’s there when you ask for it. (It might seem that top(T) is a problem, but if we assume that stacks are always generated by push operations, we see that T = push(S, e) for some S and e.)

Looking forward to visiting state-side.

Time flies when you’re having fun, I guess. Or when you’re working 24/7 on MEET. In any case, we’ve just had a respectable 1am rain shower here in Haifa, marking Enter Winter, followed by Rain and Hail a bit earlier than last year. Seemed like a good milestone to mark.

Consider it marked.

Now, back to the Java/PHP mishmash.