Code template for a postcondition contract clause. Eiffel Software ensure code Optional "then" keyword that is added by the tool when working with a feature redeclaration. The literal is empty by default and is substituted with " then" programmatically.