The best software components will be hard to use unless they are accompanied by precise accurate documentation. The talk describes some powerful notation for writing such documentation and tools that can be used to produce such documentation and check that it accurately describes the software.