On 11/9/2019 4:23 AM, Timon Gehr wrote: > You need in and out contracts for modular verification. You can pick up both from looking at the assert's in the prolog and epilog of the function. More importantly, nobody is working on a modular verification system for D, and haven't for 20 years, so the contracts aren't particularly useful.