# Tag Info

7

This is an excellent question: how do we know that a complex piece of mathematics is correct? The (by now) traditional point of view is that if we succeed in proving something then it must be correct. Unfortunately, this point of view is a tad naive. Indeed, published papers often contain wrong results, and these can remain unnoticed for decades. Some high-...

4

Now that the question has been edited to make it clearer what you are asking, there is a simple and elegant answer. The solution is: delta debugging. Delta debugging solves exactly this problem. Let me elaborate. Problem statement I am interpreting your question as asking about the following problem: We have $M$ software modules, and some way to run ...

4

No finite set of test cases can prove correctness of an algorithm, if we have no information about the form or structure of the algorithm and if the set of possible inputs is infinite. For any finite set of test cases you might have in mind, I can come up with an algorithm that works correctly on all of those test cases, but is incorrect (works incorrectly ...

4

Since you are interested in generating test sequences automatically using colored Petri nets, note that it's not clear that you need reduction to control flow graphs (and dealing with all the related issues). Some techniques were presented, that use various different methods to generate test sequences from Petri nets. Some examples include: H. Watanabe and ...

4

in my opinion, The designer of this question just wanted to make a famous algorithm problem a bit complicated but made it totally nonsense. This is the famous two egg problem where You are given two eggs and access to a 100-story building. Both eggs are identical. The aim is to find out the highest floor from which an egg will not break when dropped ...

3

Tools that solve problems like this often use a SMT (Satisfiability Modulo Theories) solver. This a SAT solver combined with a "theory solver" that can understand operations in some domain. For example, constraints involving = and != can be decided using union find; constraints involving < on numbers can be decided using the simplex algorithm. ...

3

Yes. One can construct a Majella sequence of length $n \cdot 2^n + 1$, recursively. It's easy to see you can't do any better than this, so this is optimal. Definition. I'll say that a sequence $x_0,x_1,\dots,x_m$ of $n$-bit values is a $n$-bit Majella sequence if $x_0=x_m$, and for each $y \in \{0,1\}^n$ and each value $e \in \{0,1\}^n$ with a single bit ...

3

There are many different kinds of control-flow constructs that only map to "structured programming" (tree decomposition) constructs when you add extra data variables and extra tests. continue is usually okay (as long as its not nested any deeper), but break is one of the hard ones. Another relatively painful case is short-circuit conditional evaluation. A ...

2

If you are working on "improving performance" of pseudocode, I'd tell you to forget about that. War stories of people optimizing the wrong part of a program are a dime a dozen. Perhaps the most hilarious one involved an early FORTRAN compiler for Unix. The programmer noticed a function he estimated would be called each 10 or so compilations, and took a week ...

2

This is related to a well known problem with a conjecture due to Karpovsky and Moskalev  (I still believe is open) that at most V-1 paths are needed. It is tied to conjector of Erdos, Goodman, and Posa . If you want the state of the art today, I suggest doing a thorough reverse-citation search on .  Karpovsky, M. G., and E. A. Moskalev. "...

2

You juggle with "probabilities" without defining any. There are two different questions here. For practical programs, can I use random testing to establish that any given execution has close to 100% success probability? Not in the strict sense, no. Even if input spaces are finite, they are typically huge. Without further information, you'd have to test a ...

2

I think you raise an important point, which is that in a high level language, specifications can be hard to distinguish from implementations. For example, in Coq, the specification of "The sum of the elements of a list of naturals" is probably going to look something like: Fixpoint sum (l : List Nat) : Nat := match l with | [] => 0 | x::xs => ...

2

Identify the representation invariants. Add assert statements to check that the representation invariant holds (sometimes called a repOK function). Use random testing to generate millions of test cases, and check that no assert ever fires. Build a reference implementation of the abstract data type that implements all of the methods, but instead of using ...

1

Multilinear polynomials If you're willing to use probabilistic methods, I suggest using a randomized algorithm for polynomial identity testing. You want to test whether $f(x)=g(x)$ holds for all $x$, where $f,g$ are multilinear oolynomials. This is an instance of the polynomial identity testing problem. There are effective randomized algorithms for ...

1

They are statements about patterns of correct and incorrect code: For all call sites L1, there does not exist a store site L2 such that ... (and here I’m not clear—is that L2 may follow L1? Or that the truth of the statement may follow from the program, depending on L1 and L2?) For all call sites L1, there exists a store site L2 such that ... (idem.)

1

To find out if it is e.g. doing binary search (or using hashing, or whatever) inside, you have to look at what it is doing. No way around it. Why would you insist on a particular algorithm? The whole point of modularity (and thus of much of modern programming languages and techniques) is to be able to hide such irrelevant details, and have users depend only ...

1

It's not correct to say that in TLA+, the program is the specification. I don't know of any system where that is true. Rather, TLA+ is a way of writing a formal model of a system. You could think of that as a program. Then, we want to verify some property of that program. The property must be specified separately. For instance, the model might describe ...

1

To achieve 100% coverage of all the cases, you'll probably need many test cases. You might want to do some reading on "test case generation". Typically, software developers think through the possibilities and manually write test cases that they think will exercise each code path. However, another option is to use automated tools, like symbolic execution or ...

1

If you want to automatically explore the state space of a program, you could try a fuzzer like AFL. But usually programmers do this by running the program under a debugger and thinking a bit about how the input needs to look to take a particular path through the code.

1

Shortly - no, it is not safe. Huge random test does not guarantee success (but of course, when there is a bug, it finds it in the most cases). To test threaded tree with deletion and insertion you need to have saturated all nodes (with thread links), make them change thread, the same for deletion. To make sure it works all corner cases must be covered both ...

1

The answer depends upon whether you are interested in this as a theoretical exercise or if you have a practical problem to solve. The theory There are tons of theory papers written about how to select a set of such tests. The standard catchphrase is "combinatorial testing". You should easily be able to find tons and tons of research papers, white papers, ...

Only top voted, non community-wiki answers of a minimum length are eligible