Overview

Objectives:

• Learn Go (learn some “new” programming language concepts)
• Get to know concurrent programming
• Apply formal methods
  • Formal notation/specification1
  • Program analysis
  • Static vs dynamic verification

Why? Can’t we just use AI? Well, ….

AI might great to solve for web programming but often it’s not always about “coding”.

Keep in mind:

• AI generates code
• AI does not generate specifications
• AI does not understand intent
• AI does not prove correctness
• AI does not manage responsibility

Formal methods

I enjoy writing code. I can’t be bothered with testing/verifying my code.

“AI shift”. Less focus on coding. More focus on testing/verification.

Testing example

// Scan string for two subsequent As.
func checkAA(s string) bool {
    for {
        switch {
        case s[0] == 'A' && s[1] == 'A':
            return true
        default:
            s = s[1:] // drop head
        }
    }
}

func test_case() {
    fmt.Printf("%t", checkAA("aaA B AA CC"))
}

Seems to work!

Runtime checks

func safeDiv(x int, y int) (int, bool) {
    if y == 0 {
        return 0, false
    }
    return x / y, true
}

The extra check causes some runtime overhead.

Could we remove the check? Could we statically reject programs such as safeDiv(3,0)?

Formal specifications

Let’s take a look at another programming task.

Given some string, return the longest suffix that does not contain two colons (":") in a row.

Let’s take a look at some examples first. We will use the Go programming language to specify some unit tests that represent the expected behavior.

func testExtract(extract func(string) string) {

    runTest := func(input string, expected string) {
        result := extract(input)
        if result == expected {
            fmt.Printf("\n Okay %s %s %s", input, result, expected)
        } else {
            fmt.Printf("\n Not okay %s %s %s", input, result, expected)
        }

    }

    runTest("Ha::ll::oooo", "oooo")
    runTest("47:11", "47:11")
    runTest("47::11", ":11")

}

Anything (strange) you notice?

The test (examples) contradict each other. The first example runTest("Ha::ll::oooo", "oooo") states that none of the colons shall appear in the resulting string whereas runTest("47::11", ":11") seems to match the above verbal task description.

• Who is wrong?
• The developer?
• The customer?
• The test?
• The specification?

Most real-world bugs are not implementation bugs. They are specification bugs.

We need a more formal specification of the task.

Given some string, return the longest suffix that does not contain two colons (":") in a row.

Let s = [x1,...,xn] be some string of length n.

Then, [x1,..,xi] where  i in {1,...,n} is a prefix of s.

Then, [xi,...,xn] where i in {1,...,n} is a suffix of s.


We seek the longest suffix that does not contain two colons in a row.
Formally, we seek suffix [xi,...,xn] where i in {1,...,n} is the smallest number such that
there is no k in {0,...,n-i-1} where xi+k == ':" and xi+k+1 == ':'.

Example. Consider the string “:Ha:_:ll::oooo”.

Implementation

Here is an implementation of the task in Go.

func extractLongestSuffix(s string) string {
    var i int
    i = len(s) - 1

    for {
        switch {
        case i < 1:
            return s
        case s[i] == ':' && s[i-1] == ':':
            return s[i:]
        default:
            i--
        }
    }

}

How do we know the above implementation is correct? We could run extractLongestSuffix against some test cases.

How many test cases do we need?

Writing test cases is painful. Is there a more clever way?

Yes! The formal methods literature offers heaps of methods. For example, consider QuickCheck style testing. The idea is as follows:

• Specify some property that holds for all input values

• Generate some input data and check if the property holds

Concurrent programming

The world is concurrent.

Microservice written in Go

Full program code is available here

func cost() (int, bool) {
    ch := make(chan int)
    go func() {
        ch <- getDiscount()
    }()
    x, err := getBaseCost()
    if err {
        return 0, false
    }
    y := <-ch
    cost := compCost(x, y)
    return cost, true
}

• Compute the cost of some product
• Computing the base cost and some discount is done concurrently

What could possibly go wrong?

There is some hidden blocking bug