This chapter describes all the constructs with which you can write more advanced expressions, ranging from expressions that can be used only in postconditions to definitions of variables that are local to a context definition.