How to write precondition in pseudo code

Question

I was just wondering if anyone knew how to represent a pre-condition in pseudo code as I have had a look around can not find anything on the subject.

Thank you

Answer 1

Pseudo-code, is, by definition, not formalized code. An example of using pseudo-code to define a precondition for a C# method would be:

// Precondition: Object must have been initialized by calling init() or by
// manually setting properties X and Y such that X.Foo >= Y.Bar.
public void doUsefulWork() {
    ...
}

Clearly, since pseudo-code is not formalized, it cannot be verified by the compiler.

• It's the duty of the user of the method to ensure that the preconditions are met, and
• it's the duty of the developer of the method to acknowledge that changing the precondition is (usually) a breaking change.

Answer 2

I see here two possibilities:

1. If you can formulate your conditions into real code, I would give Programming With Assertions a try (or the .NET equivalent Debug.Assert). This way you can actually let the your conditions be checked during run time with assert condition

2. If this is not the case or you simply don't want to, you could write the pre- and post condition into your JavaDoc.

   /**
    * @precondition: the connection has been established.
    * 
    * @postcondition: the schema is created.
    * 
    */
   

You could even define these JavaDoc annotations so they appear in the JavaDoc-generated documentation. This way you can use natural language you define what you want to assert.

You could also express your pre- and postconditions more mathematically I order to increase the succinctness of your conditions, which might make them more understandable:

For simple number comparisons you can surely use <, <=, >, >=, etc. But let's say you want to define the invariant for a Set then you could express it as:

/**
  * @invariant: set == filterDuplicates(set)
  *
  */

Thus making use of hypothetical/pseudo functions to express your conditions.

This can be developed even further if you are fond of functional languages. My data structure and algorithms professor used Haskell to define precondition, postcondition and invariants for newly introduced data structures:

module TreeSets(TreeSet, 
                contains, add, remove, card, traverse)
where
data Ord t => TreeSet t = E | N (TreeSet t) t (TreeSet t)

inv E = True
inv(N l x r) = all(<x)(abs l) && all(>x)(abs r) &&
   inv l && inv r

It really depends for whom you are writing this, hence my recommendation is to use natural language. It can be understood by everyone and is especially for object-oriented programs the easiest to formulate.