Microsoft IntelliTest (formerly Pex) [1] is internally using Z3 constraint solver that traces program data and control flow graph well enough to be able to generate desired values to reach given statement of code. It can even run the program to figure out runtime values. Hence the technique is called Dynamic Symbolic Execution [3]. We have technology for this, just not yet applied correctly.
I would also like to be able to point at any function in my IDE and ask it:
- "Can you show me the usual runtime input/output pairs for this function?"
- "Can you show me the preconditions and postconditions this function obeys?"
There is plenty of research prototypes doing it (Whyline [4], Daikon [5], ...) but sadly, not a tool usable for the daily grind.
Microsoft IntelliTest (formerly Pex) [1] is internally using Z3 constraint solver that traces program data and control flow graph well enough to be able to generate desired values to reach given statement of code. It can even run the program to figure out runtime values. Hence the technique is called Dynamic Symbolic Execution [3]. We have technology for this, just not yet applied correctly.
I would also like to be able to point at any function in my IDE and ask it:
- "Can you show me the usual runtime input/output pairs for this function?"
- "Can you show me the preconditions and postconditions this function obeys?"
There is plenty of research prototypes doing it (Whyline [4], Daikon [5], ...) but sadly, not a tool usable for the daily grind.
[1] https://learn.microsoft.com/en-us/visualstudio/test/intellit...
[2] https://link.springer.com/chapter/10.1007/978-3-642-38916-0_...
[3] https://queue.acm.org/detail.cfm?id=2094081
[4] https://www.cs.cmu.edu/~NatProg/whyline.html
[5] https://plse.cs.washington.edu/daikon/