I used to do this with a method kind of like Cleanroom with inspiration from formal specs and refinement, too. You have to be able to figure out the specifics a

I used to do this with a method kind of like Cleanroom with inspiration from formal specs and refinement, too. You have to be able to figure out the specifics ahead of time without explorative execution. From there, I used decomposition noting the inputs, outputs, and so on of each function. I used a subset of a programming language with predictable behavior that maps to that. I'd usually know what's going to happen before it happened by just walking through the program in my head. Main problem was third-party libraries, which I had to profile ahead of time. Or just use a friggin' computer since even that wasn't reliable for those in C. Here's a write-up on Cleanroom: http://infohost.nmt.edu/~al/cseet-paper.html http://infohost.nmt.edu/~al/cseet-paper.html Here's a test of it by NASA around 1990 where the E.3 and E.4 sections highlight its benefits and requirements: https://ntrs.nasa.gov/archive/nasa/casi.ntrs.nasa.gov/19910008271.pdf https://ntrs.nasa.gov/archive/nasa/casi.ntrs.nasa.gov/199100...