Uche Ogbuji on Object-Oriented Programming Languages

From a post to the xml-dev news group in 2002:

I do strongly agree that C++ and Java have pretty much given OO a bad name. Meyer's work in Eiffel proves that OO did not need to ditch axioms from abstract data types. Kay's work in Smalltalk proves that OO did not need to ditch dynamicism. Stroustroup started out with a solid, practical core and made too little fuss as a committee ruined it. Joy, as far as I can tell by the language he spawned, enjoyed strapping straitjackets onto paramedic training dummies.

Two for the Price of One

Yesterday I was out shopping with my daughter and we got to discussing a price tag that said "Two for the Price of One".  She asked "What would it cost if you wanted 3?" and I explained that you could work it out by splitting the 3 into 2 + 1.  The "Two for One" would only apply to the 2, and you would have to pay the full price for the 1.  I then summed it up as "Half Price for Even Quantities".  Thinking about this now, a better way to sum it up would be as (p div 2) + (p mod 2), where p is the original price in pennies.

The Die Hard Problem in Alloy 3

In the examples included with the TLA+ Tools distribution, Leslie Lamport includes a solution to the so-called Die Hard Problem:

In the movie Die Hard 3, the heros must obtain exactly 4 gallons of water using a 5 gallon jug, a 3 gallon jug and a water faucet.

Today, as an excercise in using the natural numbers in Alloy, I translated the TLA+ solution into Alloy 3:

 module tristram/diehard
   
   open util/natural
   open util/ordering[State] as SO
   
   /* Define names for Natural numbers Two to Five 
      (Zero and One are defined in util/natural):
   */
   lone sig Two in Natural {}
   lone sig Three in Natural {}
   lone sig Four in Natural {}
   lone sig Five in Natural {}
   fact {
     Two = inc(One)
     Three = inc(Two)
     Four = inc(Three)
     Five = inc(Four)
   }
   
   sig State {
     small : Natural,
     big : Natural
   }
   
   pred init(s : State) {
     s.small = Zero
     s.big = Zero
   }
   
   pred emptysmall(s, s' : State) {
     s'.small = Zero
     s'.big = s.big
   }
   
   pred emptybig(s, s' : State) {
     s'.small = s.small
     s'.big = Zero
   }
   
   pred fillsmall(s, s' : State) {
     s'.small = Three
     s'.big = s.big
   }
   
   pred fillbig(s, s' : State) {
     s'.small = s.small
     s'.big = Five
   }
   
   pred smalltobig(s, s' : State) {
     let t = add(s.small,s.big) |
       s'.big = if util/natural/lt(t, Five) then t else Five
     s'.small = sub(s.small, sub(s'.big, s.big))
   }
   
   pred bigtosmall(s, s' : State) {
     let t = add(s.small, s.big) |
       s'.small = if util/natural/lt(t, Three) then t else Three
     s'.big = sub(s.big, sub(s'.small, s.small))
   }
   
   fact Traces {
     init(SO/first())
     all s : State - SO/last() |
       let s' = SO/next(s) |
         emptysmall(s, s') or
         emptybig(s, s') or
         fillsmall(s, s') or
         fillbig(s, s') or
         smalltobig(s, s') or
         bigtosmall(s, s')
   }
   
   pred show() {
     SO/last().small = Four or
     SO/last().big = Four
   }
   
   /* 7 is the smallest scope for States that gives a solution.
      This was found by progressively increasing the scope.
      We need scope 9 for the naturals (0..8) because smalltobig 
      and bigtosmall use the sum of s.small and s.big:
   */
   run show for 7 but 9 Natural
   

A New Version of Alloy

Beta versions of version 4 of the Alloy Analyzer are available from here.  This version includes some changes to the syntax of the Alloy language (see here), which is unfortunate since it makes Daniel Jackson's new book obsolete only 6 months after it was published.  However, updating models from version 3 to version 4 syntax does seem to be fairly easy. Still, it might be a good idea to have Alloy 3 and Alloy 4 installed alongside each other, at least until you have got used to the new version.

Why Alloy has no in-built Notion of State

A few years ago Daniel Jackson took the rather surprising step of actually removing in-built support for states from the Alloy specification language. Here he explains why:

the main advantage of the old scheme was that, with the notion of pre and post built in, certain mutability constraints could be built in too. when you declared a state component, you could say how it changed.

but it turns out that priming as an operator is much more complicated than you would imagine. it made for all kinds of kludges in the implementation, which was a sure sign that the semantics was too complicated. and sure enough, if you take a look at the semantics of sequential composition in the Z standard, you'll see that it's full of subtle details and is really quite ad hoc.

the main reason we dropped it, tho, was that we wanted to be able to handle dynamic behaviour with more flexible idioms. with that priming convention, you're really tied to a rather narrow way of writing models. having got rid of it, we can do more ambitious things -- talking about sequences of more than a pair of states, for example.

(From the alloy-discuss group.)

One of the reasons that I became disillusioned with Z and its object-oriented extensions was that they had become bogged down in a state-based view of specification. This seemed to me to be so limiting. It was as if the developers of Z were satisfied with just aping programs. They didn't seem to be interested in going any further. I wanted more, and I am glad to see that Daniel Jackson does too.