Month: April 2005

A sign of things to come?

I got the following in an email disclaimer that foreshadows interesting times ahead:

This email and any files transmitted with it are confidential and intended solely for the use of the individual or entity to whom they are addressed.

Sounds like humans are only part of the game these days, and “entities” will be asserting their rights more forcefully in future. Perhaps such entities represent affiliated groups of humans, but perhaps they represent other semi-sentient information agregates such as software agents or epi-phenomena growing out there on the web as viruses or telephone exchanges?

One Question – How many of you reading this fall into the non-human category?

Thanks to GlennD for this signpost to the future

Straw Poll

I’m thinking of getting myself a new machine. If it was you and you were going to buy a tablet PC… which would it be?
And if it was a plain old laptop (desktop replacement)?
And workstation?

Hmmmm. Let me know, cos I’m stumped!

Now I know…

… why people are so keen to be famous:

Because when you’re famous you can burn your bridges.

I happen to want to burn mine so much right now, that I could spit! What was I thinking? Tomorrow would have been my last day. It still could be, but I can’t just walk out, cos that would mean I might get a bad reference, which I can’t afford.


Gross quote of the day

Your baby is now nearly 3 inches long – about the size of a jumbo shrimp – and weighs nearly an ounce.

Kerry must a have her own little rock pool developing…

…so long as there’s no crabs everything is OK.

Predicates and Expressions – Part 2

Last time I started discussing the expression language used to define predicates on types and members. My conclusions were:

  • C# expression syntax used since code must be transformed to that in the end, and the more similar the syntaxes of the expression language – the easier the transformation will be.
  • No side-effects. Side effect within the predicates complicate the tasks of determining whether a temporal comparison is actually effective. If the snapshots can't be guaranteed to be faithful representations of the state before and after the test, then you can't trust the tests, and you might as well not have bothered with them in the first place.
  • Pragmas, or pre-processor messages, are used in expressions to add a temporal ability to the predicates. $before(foo) allows a snapshot of the variable foo to be taken for later comparison with the exit state.
  • Pragmas may map to identity in some circumstances. Entry states can have no $after() since we haven't reached the exit state yet. Likewise, there is no notion $before() state since this is the before state, and we can't take a snapshot of the state before the before state (unless it's on some other superior method). Therefore, in a precondition it should be illegal to insert pragmas into predicate expressions. In some cases such as $before(foo) in a precondition, and $after(bar) in a post condition the pragmas map onto the current value of the variable. i.e. in a post condition $after(bar) can be transformed into bar.

The algorithm for converting predicates to guard code is shown below.

foreach assembly in assembly list
  foreach type in assembly
    clear list of invariance predicates
    clear list of processed methods
    foreach invariant attribute on type
      transform pragmas on predicate
      add pre/post analysis objs to list
      generate code for predicate
      append code to processedInvariants list
    end foreach invariant
    foreach member in type
      clear list of requires attrs
      foreach requires attr on member
        transform pragmas on predicate
        add pre/post analysis objs to list
        generate code for predicate
        append code to processedRequires list
      end foreach requires attr
      clear list of ensures attrs
      foreach ensures attr on member
        transform pragmas on predicate
        extract list of vars to be snapshot
        add to list processedSnapshots
        add pre/post analysis objs to list
        generate code for predicate
        append code to processedEnsures list
      end foreach ensures attr
      insert snapshots into code template
      insert pre/post analysis objs to template
      insert code for requires guards into template
      insert code for ensures guards into template
      generate code
      add generated code to processed methods list
    end foreach member
    insert code for members into type template
    clear list of invariance predicates
    generate code for type
    append code to processed types list
  end foreach type
  setup c# compiler with config params
  compile all types in processed types list
  store assembly as per instructions
end foreach assembly

This algorithm conveniently glosses over the complexities of the depth first search event propagation mechanism described in previous posts, but the outcome is the same ultimately.

Predicates and Expressions – Part 1

The predicates that are used to specify the in, out and inv conditions on a component need to follow certain rules. The first and least obvious is that it must follow the syntax and semantic rules of the C# language. I say that it is the least obvious, since it seems to be conventional to invent a new predicate language for these purposes. I can see the point of this, since it would allow a tailor made language to be used, and to extend it beyond the capabilities of a normal C# expression. I intend to start off with the syntax of C# because they will have to end up as C# expressions, and I want to have to intervene in the simplest way possible. I want the intervention to be achievable via regex replacements where possible.

It it essential to make one significant enhancement to the expression language of C#. It needs to be temporal. It needs to be able to make statements about the value of a variable before and after a method has been invoked. In a temporal logic that might be represented by a prime (i.e. x'). That could get rather confusing when we are making comparisons with characters that need to be enclosed by single quotes. At the very least it would be hard to read. Likewise we could represent it as a function which can be made available through a supertype or a utility object. An expression might resemble this: "before(x) == after(x) – 1". The problem is that this pollutes the method namespace so we would have to have something like this in the expressions: "base.before(x)". Which is already looking ugly, and it also forces the user to inherit from a supertype that may wreck their application design.

It seems that we need pragmas – preprocessor directives that can be used as clues to the framework. Since we are using the syntax of C# we can be sure that neither types nor member names will begin with a dollar sign. It seems safe to assume that we can begin pragmas with a dollar sign like so: "$before(x) == $after(x) + 1". It should not be confused with interpreted scripting language though, this is input for a pre-processor that outputs code, which is subsequently compiled. That applies whether we are performing dynamic code generation.

The sharp-eyed of you will notice that in various kinds of predicate the $before(x) and $after(x) are synonymous with x itself. For example it makes no sense to refer to a $after(x) in a requires predicate. Likewise, there isn't much use for an $after() pragma since we are inserting code into the method of a target object. x will already embody the value in $after(x) so the $after() will just be getting in the way. So, we only need a $before(x) pragma
to take a snapshot of the value of the variable at the beginning of the method, for later comparison with what the variable becomes.

There are some rules that predicates must obey, and we just saw one of them before. In a pre-condition, $before(x) and x are synonymous, and therefore $before() is meaningless, and shouldn't be found there. This sort of rule can be detected and converted into harmless code by the preprocessor. Another hard and fast rule is that predicates must never have side-effects. That is – the state before testing the predicate should be exactly the same as the state after the test. There are circumstances in which that is untrue. If a predicate detects a bug, it may throw an exception, which may cause the stack to unwind, which will have a side effect. But that is a desired side effect that is part of the semantics of design by contract and error detection, as well as being permissible in a constant method (assuming such a thing were possible in C#). What I mean is undesired side-effects – side effects that are not implicit in the error checking framework, and which are not testable by the predicates themselves.

There is a need to avoid harmful code that is harder to spot. The predicates should be without side-effects. It's easy enough to spot when someone accidentally inserts a "=" instead of a "==", but if they code a helper method such as "IsOkToDoIt(this)" that happens to change a variable as it runs, then the predicates change from being an external test of correctness into another kind of source code. We need to prevent this – we are interested in making statements about the state of the class, and how it changes from moment to moment. We don't need to be concerned with making changes to it, since that is what the component code is for.

There is no way to prevent the predicates from having a side effect. Fullstop! Surprisingly C# doesn't support the ability to define constant methods. Constant methods are a powerful feature in the armoury of the C++ library writer. It makes it possible to assert the fact that a method has no side effects. In C# you are not able to make that kind of assertion. So we will just have to make it known to the DBC-driven programmer that coding predicates that have side-effects is asking for misery.