markupTitle DrNim User Guide drnim.html DrNim User Guide 0 heading Introduction drnim.html#introduction Introduction 0 heading Installation drnim.html#installation Installation 0 heading Motivating Example drnim.html#motivating-example Motivating Example 0 heading Pre-, postconditions and invariants drnim.html#preminus-postconditions-and-invariants Pre-, postconditions and invariants 0 idx requires drnim.html#requires_1 Pre-, postconditions and invariants 0 idx ensures drnim.html#ensures_1 Pre-, postconditions and invariants 0 idx invariant drnim.html#invariant_1 Pre-, postconditions and invariants 0 idx assume drnim.html#assume_1 Pre-, postconditions and invariants 0 heading Invariant drnim.html#preminus-postconditions-and-invariants-invariant Invariant 0 heading Requires drnim.html#preminus-postconditions-and-invariants-requires Requires 0 idx precondition drnim.html#precondition_1 Requires 0 heading Ensures drnim.html#preminus-postconditions-and-invariants-ensures Ensures 0 idx postcondition drnim.html#postcondition_1 Ensures 0 heading Assume drnim.html#preminus-postconditions-and-invariants-assume Assume 0 heading Example: insertionSort drnim.html#examplecolon-insertionsort Example: insertionSort 0 heading Syntax of propositions drnim.html#syntax-of-propositions Syntax of propositions 0