Text this: Deductive Software Verification – The KeY Book