if (var == true) {
    ...
} else if (var == false) {
    ...
} else {
    ...
}

if (var == true) {
    ...
} else if (var == false) {
    ...
} else {
    ...
}

if (var == true) {
    ...
} else {
    ...
}

if (var != true || var != false) {
    errorReport("Hell just frose over, var must be true or false")
}
......
if (var == true){
 ....
} else {
 ....
}

// Assign 3 to x
var x = 3;
x = 3;   // again, just for sure
while (x < 3 or x > 3) { x = 3; }  // being robust
if (x != 3) { ... }  // this got to be an error!

class List:
  def __init__(self, items):
    self.__size = len(items)
    self.__data = items

  def __invariant(self):
    assert self.__size == len(self.__data)

  def size(self):
    self.__invariant()

    return self.__size

  def at(self, index):
    """index should be in [0,size)"""
    self.__invariant()
    assert index >= 0 and index < self.__size

    return self.__data[index]

  def pushback(self, item):
    """the subsequent list is one item longer
       the item can be retrieved by self.at(self.size()-1)"""
    self.__invariant()

    self.__data.append(item)
    self.__size += 1

    self.__invariant()
    assert self.at(self.size()-1) == item

Spec: If var is false then the function does "this", otherwise it does "that".

if (var == false) dothis; else dothat;

for (int i = 0; i != sequence.length(); ++i) {
    // do something with sequence[i]
}

for (int i = 0; i < sequence.length(); ++i) {
    // do something with sequence[i]
}