Nicolas, are you aware of SAT-SMT solvers? (SAT/SMT by Example
(sat-smt.codes) <https://sat-smt.codes/SAT_SMT_by_example.pdf>) Microsoft
used Z3 to great effect in flushing out bugs in Vista. SAT-SMT's used in a
thing called Concolic testing - Wikipedia
<https://en.wikipedia.org/wiki/Concolic_testing>,

frank

On Mon, 17 May 2021 at 05:14, Nicolas Cellier <
nicolas.cellier.aka.nice at gmail.com> wrote:

> More seriously, there is not a single kind of test.
> One category is kind of specification illustrating the expectations,
> and demonstrating how to use some message/class.
> Most of the time, our tests as specification lack the quantifiers
> (like the universal quantifier), that's why I name them illustrating.
> Ideally, we would like to have some form of formal proof, but there
> rarely is one accessible, unless we drastically restrict the
> capabilities (like recursivity and all forms of reflexivity)
> At least, that's my understanding of
> https://en.wikipedia.org/wiki/Formal_methods
>
> In some rare cases, we now have enough computing power to test an
> implementation exhaustively (like a function of a single float32
> argument).
> Alternatively, we can try and test with randomly generated inputs, but
> that's a bit like shooting in the dark.
>
> In order to be more eager, we sometimes write tests against a specific
> implementation with specially crafted examples for non regression or
> main gotchas of the specific algorithm.
> I guess my efforts fall in such a category: it's kind of adversarial
> strategy; somehow like a game of finding the shortcomings.
> If we have watts to burn, I think that it would be interesting to use
> machine power to find and construct those adversarial examples, not
> based on sole randomness, but some form of analysis of algorithms and
> probably some set of heuristics.
> How could we build such machinery, I don't know, for now it's still
> buzzwords.
>
> Le lun. 17 mai 2021 à 12:00, Nicolas Cellier
> <nicolas.cellier.aka.nice at gmail.com> a écrit :
> >
> > Le dim. 16 mai 2021 à 17:10, David T. Lewis <lewis at mail.msen.com> a
> écrit :
> > >
> > > On Fri, May 07, 2021 at 07:39:50PM +0000, commits at source.squeak.org
> wrote:
> > > > Nicolas Cellier uploaded a new version of Kernel to project The
> Trunk:
> > > > http://source.squeak.org/trunk/Kernel-nice.1402.mcz
> > > >
> > > >
> > > > Musing is more powerful than dumb static and coverage tests, I wish
> I got more time for musing :)
> > > > We deadly need evolutive testing (neural based).
> > > >
> > >
> > > Interesting commit comment. How might this work?
> > >
> > > Dave
> > >
> > >
> > Hi Dave,
> > How? This way: put enough buzzwords in commit comments to bring some
> > academics on the subject ;)
>
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.squeakfoundation.org/pipermail/squeak-dev/attachments/20210517/aeb54c2e/attachment.html>