On Fri, Nov 25, 2016 at 12:30 AM Michael Jones <michael.jo...@gmail.com> wrote:
> This is very nice! However, am i right in understanding that the magic is > in knowing the text of the program--the fact that there are untaken > branches? If so, this is not simply a 'behavioral' verification...it knows > about the construction of the code and not just its behavior. Maybe I was > unclear. > > Indeed you are right. This requires the ability to work on the program text. It is a bit too hard to work on the output assembly for the program. The advantage of a model-checker or a probalistic method such as "testing/quick" is that they regard the system-under-test as a black box. This fact can be used in numerous ways. The most powerful one is that once you have a specification model, in *any* programming language, it applies to any system implementing that model, in *any* language. This has been used historically for checking protocols for correctness, where the specification were written in some high-level language (Haskell, Erlang) but the code being tested were run in a low-level language (C, typically). In short, no single method applies in every case. Figuring out if two programs are observationally equivalent usually requires one to exploit the structure of the program text. Because from that structure the proof or search strategy can be extracted. -- You received this message because you are subscribed to the Google Groups "golang-nuts" group. To unsubscribe from this group and stop receiving emails from it, send an email to golang-nuts+unsubscr...@googlegroups.com. For more options, visit https://groups.google.com/d/optout.
