Archive for April, 2005
It may have survived being slashdotted, but I will now attempt to crush this site with the countless referrals from my own pangalactic blog.
Go there and use your force for evil.
Hwah Hwah Hwah !!!
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
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)?
Hmmmm. Let me know, cos I’m stumped!
… 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.
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.
Last time I started discussing the expression language used to define predicates on types and members. My conclusions were:
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.
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.