Introduction

We introduce informal notation that can be maintained in comments together with formal Slang notation. The reason for this is that the systematic notation for the concepts we discuss is useful beyond their use in Slang. Of course, Logika offers automated support for reasoning about these concepts in Slang. We believe that even if such support is not available, rigorous informal reasoning already goes a long way and provides a good way to embed pertinent correctness arguments in the documentation.