Per VognsenSince he has just passed away, I was trying to find a free PDF link of my favorite Hoare paper, Proof of Correctness of Data Representations, but unfortunately it is under the Springer iron dome. You can enter the DOI 10.1007/3-540-07994-7_54 into your preferred website for liberating scientific information.
This is his paper on abstraction functions for concrete implementations of abstract data types. It was hugely influential and the ideas are also more directly applicable to programming practice than Hoare logic style proofs (as someone who uses informal Hoare logic proofs all the time, that is not a dis).
Sharlock93@pervognsen I remember the asserts on the invariants for parts of ion. That style of thinking about operation having preconditions or invariants has been super helpful for me. (I hope I'm not mixing up preconditions and invariants)