<div dir="ltr"><div dir="ltr"><div class="gmail_default" style="font-family:arial,helvetica,sans-serif"><span style="font-family:Arial,Helvetica,sans-serif">On Mon, Dec 10, 2018 at 1:03 PM Frans Schneider <<a href="mailto:fchschneider@gmail.com">fchschneider@gmail.com</a>> wrote:</span><br></div><div class="gmail_quote"><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex"> I don't want <span class="gmail_default" style="font-family:arial,helvetica,sans-serif"></span>to make changes to the application's code base to facilitate testing <br>
because that would give to much clutter.<br>
</blockquote><div> <br></div><div><div class="gmail_default" style="font-family:arial,helvetica,sans-serif">I'd beg you reconsider this stance.</div><div class="gmail_default" style="font-family:arial,helvetica,sans-serif"><br></div><div class="gmail_default" style="font-family:arial,helvetica,sans-serif">In my experience, adding tooling around an application in order to query its internal state in a well-defined way is often beneficial when there is a bug and you need to introspect the code in question. Debugging is often helped by having a canonical way to inspect and analyze the application. Also, if you need to run through hoops before you can test your code, chances are you are looking at the wrong API, so it should at least be entertained a better one might exist.</div><div class="gmail_default" style="font-family:arial,helvetica,sans-serif"><br></div><div class="gmail_default" style="font-family:arial,helvetica,sans-serif">In linear logic, there are two kinds of choice called "additive conjunction" and "additive disjunction". One type, conjunction, is controlled by either the PropER model or by the caller into the application/SUT. The other kind of choice, disjunction, is made by the application/SUT internally when it executes. Additive disjunctions are hard because they make the model unable to predict what will happen. So it has to guard against all types of outcome from the SUT/application, and this makes the models quite weak. The Wikipedia page has a nice example with a vendoring machine interpretation of the model[0], but the idea of a linear dialogue between a buyer and a vendoring machine is exactly mapped into an API user and the process behind the API, implementing it.</div><div class="gmail_default" style="font-family:arial,helvetica,sans-serif"><br></div><div class="gmail_default" style="font-family:arial,helvetica,sans-serif">One important point about PropER testing is that you must try to shift as much choice to be controlled by the model. This often requires an API where one can inject parameters from the outside to control the setup of certain states. You can always have a sane default which initializes if not overriden, and this is what I've often done. Important examples are that randomness and time must be controlled from the outside in some way. Otherwise, the system tend to become impossible to test. And it also hides important details to the user of the API to boot.</div><div class="gmail_default" style="font-family:arial,helvetica,sans-serif"></div><div class="gmail_default" style="font-family:arial,helvetica,sans-serif">[0] <a href="https://en.wikipedia.org/wiki/Linear_logic">https://en.wikipedia.org/wiki/Linear_logic</a></div><br></div></div></div></div>