Spell checking + changes some definitions

[AllanBlanchard]

• use verification condition instead of proof obligation
• use conforms to specification instead of respect the specification
• massive spellcheck with ltex