Write down every guarantee before you write any code

Here is every promise a to-do list makes. VARIABLE tasks Init == tasks = [i \in Ids |->...