Skip to main content
Bounty Ended with 50 reputation awarded by Stas Bichenko
added 349 characters in body
Source Link
Ext3h
  • 1.4k
  • 9
  • 12

No testing whatsoever is going to be able to be sufficient in this case, not even tons of real world data or fuzzing. A 100% code coverage, or even 100% path coverage is insufficient to test recursive functions.

Either the recursive function stands up to a formal proof (shouldn't be that difficult in this case), or it doesn't. If the code is too intertwined with application specific code to rule out side effects, that's where to start.

The algorithm itself sounds like a simple flooding algorithm, similar to a simple broad first search, with the addition of a blacklist which must not intersect with the list of visited nodes, run from all nodes.

foreach nodes as node
    foreach nodes as tmp
        tmp.status = unmarked

    tovisit = []
    tovisit.push(node)
    node.status = required

    while |tovisit| > 0 do
        next = tovisit.pop()
        foreach next.requires as requirement
            if requirement.status = unmarked
                tovisit.push(requirement)
                requirement.status = required
            else if requirement.status = blacklisted
                return false
        foreach next.collides as collision
            if collision.status = unmarked
                requirement.status = blacklisted
            else if requirement.status = required
                return false
return true

This iterative algorithm fulfills the condition that no dependency may be required and blacklisted at the same time, for graphs of arbitrary structure, starting from any arbitrary artifact whereby the starting artifact is always required.

While it may or may not be as fast as your own implementation, it can be proven that it terminates for all cases (as for each iteration of the outer loop each element can only be pushed once onto the tovisit queue), it floods the entire reachable graph (inductive proof), and it detects all cases where an artifact is required to be required and blacklisted simultaneously, starting from each node.

If you can show that your own implementation has the same characteristics, you can prove correctness without resulting to unit testing. Only the basic methods for pushing and popping from queues, counting queue length, iterating over properties and alike need to be tested and shown to be free of side effects.

EDIT: What this algorithm does not prove, is your graph being free of cycles. Directed acyclic graphs are a well researched topic though, so finding a ready made algorithm to prove this property should be easy as well.

As you can see, there is no need to reinvent the wheel, at all.

No testing whatsoever is going to be able to be sufficient in this case, not even tons of real world data or fuzzing. A 100% code coverage, or even 100% path coverage is insufficient to test recursive functions.

Either the recursive function stands up to a formal proof (shouldn't be that difficult in this case), or it doesn't. If the code is too intertwined with application specific code to rule out side effects, that's where to start.

The algorithm itself sounds like a simple flooding algorithm, similar to a simple broad first search, with the addition of a blacklist which must not intersect with the list of visited nodes, run from all nodes.

foreach nodes as node
    foreach nodes as tmp
        tmp.status = unmarked

    tovisit = []
    tovisit.push(node)
    node.status = required

    while |tovisit| > 0 do
        next = tovisit.pop()
        foreach next.requires as requirement
            if requirement.status = unmarked
                tovisit.push(requirement)
                requirement.status = required
            else if requirement.status = blacklisted
                return false
        foreach next.collides as collision
            if collision.status = unmarked
                requirement.status = blacklisted
            else if requirement.status = required
                return false
return true

This iterative algorithm fulfills the condition that no dependency may be required and blacklisted at the same time, for graphs of arbitrary structure, starting from any arbitrary artifact whereby the starting artifact is always required.

While it may or may not be as fast as your own implementation, it can be proven that it terminates for all cases (as for each iteration of the outer loop each element can only be pushed once onto the tovisit queue), it floods the entire reachable graph (inductive proof), and it detects all cases where an artifact is required to be required and blacklisted simultaneously, starting from each node.

If you can show that your own implementation has the same characteristics, you can prove correctness without resulting to unit testing. Only the basic methods for pushing and popping from queues, counting queue length, iterating over properties and alike need to be tested and shown to be free of side effects.

No testing whatsoever is going to be able to be sufficient in this case, not even tons of real world data or fuzzing. A 100% code coverage, or even 100% path coverage is insufficient to test recursive functions.

Either the recursive function stands up to a formal proof (shouldn't be that difficult in this case), or it doesn't. If the code is too intertwined with application specific code to rule out side effects, that's where to start.

The algorithm itself sounds like a simple flooding algorithm, similar to a simple broad first search, with the addition of a blacklist which must not intersect with the list of visited nodes, run from all nodes.

foreach nodes as node
    foreach nodes as tmp
        tmp.status = unmarked

    tovisit = []
    tovisit.push(node)
    node.status = required

    while |tovisit| > 0 do
        next = tovisit.pop()
        foreach next.requires as requirement
            if requirement.status = unmarked
                tovisit.push(requirement)
                requirement.status = required
            else if requirement.status = blacklisted
                return false
        foreach next.collides as collision
            if collision.status = unmarked
                requirement.status = blacklisted
            else if requirement.status = required
                return false
return true

This iterative algorithm fulfills the condition that no dependency may be required and blacklisted at the same time, for graphs of arbitrary structure, starting from any arbitrary artifact whereby the starting artifact is always required.

While it may or may not be as fast as your own implementation, it can be proven that it terminates for all cases (as for each iteration of the outer loop each element can only be pushed once onto the tovisit queue), it floods the entire reachable graph (inductive proof), and it detects all cases where an artifact is required to be required and blacklisted simultaneously, starting from each node.

If you can show that your own implementation has the same characteristics, you can prove correctness without resulting to unit testing. Only the basic methods for pushing and popping from queues, counting queue length, iterating over properties and alike need to be tested and shown to be free of side effects.

EDIT: What this algorithm does not prove, is your graph being free of cycles. Directed acyclic graphs are a well researched topic though, so finding a ready made algorithm to prove this property should be easy as well.

As you can see, there is no need to reinvent the wheel, at all.

Source Link
Ext3h
  • 1.4k
  • 9
  • 12

No testing whatsoever is going to be able to be sufficient in this case, not even tons of real world data or fuzzing. A 100% code coverage, or even 100% path coverage is insufficient to test recursive functions.

Either the recursive function stands up to a formal proof (shouldn't be that difficult in this case), or it doesn't. If the code is too intertwined with application specific code to rule out side effects, that's where to start.

The algorithm itself sounds like a simple flooding algorithm, similar to a simple broad first search, with the addition of a blacklist which must not intersect with the list of visited nodes, run from all nodes.

foreach nodes as node
    foreach nodes as tmp
        tmp.status = unmarked

    tovisit = []
    tovisit.push(node)
    node.status = required

    while |tovisit| > 0 do
        next = tovisit.pop()
        foreach next.requires as requirement
            if requirement.status = unmarked
                tovisit.push(requirement)
                requirement.status = required
            else if requirement.status = blacklisted
                return false
        foreach next.collides as collision
            if collision.status = unmarked
                requirement.status = blacklisted
            else if requirement.status = required
                return false
return true

This iterative algorithm fulfills the condition that no dependency may be required and blacklisted at the same time, for graphs of arbitrary structure, starting from any arbitrary artifact whereby the starting artifact is always required.

While it may or may not be as fast as your own implementation, it can be proven that it terminates for all cases (as for each iteration of the outer loop each element can only be pushed once onto the tovisit queue), it floods the entire reachable graph (inductive proof), and it detects all cases where an artifact is required to be required and blacklisted simultaneously, starting from each node.

If you can show that your own implementation has the same characteristics, you can prove correctness without resulting to unit testing. Only the basic methods for pushing and popping from queues, counting queue length, iterating over properties and alike need to be tested and shown to be free of side effects.