Reasoning About Programs - Lecture 1 Notes

Course Introduction: Reasoning About Programs

Introduction

  • Course focuses on systematically reasoning about code to ensure correctness.
  • Moves beyond testing and debugging to treat code as a mathematical object.
  • Aims to enhance code understanding and improve programming skills.

The Difficulty of Achieving Program Correctness

  • Quote from Carol Morgan (UNSW) highlights the common experience of initial programming success followed by persistent errors.
  • The challenge of creating programs that are fully correct and fail-proof is emphasized.

Binary Search Experiment

  • John Bentley's experiment: Programmers at Bell Labs and IBM were asked to write binary search.
  • Binary search algorithm: Efficiently searches a sorted array by repeatedly dividing the search interval in half.
  • O(logn)O(log n) time complexity compared to linear search.
  • Experiment result: 90% of programmers had bugs in their binary search code.
  • Carol Morgan's experiment with fourth-year computer science students at UNSW yielded similar results.
  • These experiment underscores the difficulty of writing correct code, even for well-known algorithms.

Zoom MP3 Player Bug

  • In 2006, Microsoft released the Zoom MP3 player to compete with Apple's iPod.

  • On New Year's Eve 2008, all Zoom players froze due to a software bug.

  • The bug was in the code responsible for calculating the current year, based on the number of days since 1980.

  • The incorrect code:

    while (days > 365) {
    if (isLeapYear(year)) {
        if (days > 366) {
            days -= 366;
        }
    } else {
        days -= 365;
    }
    year++;
}

  • The issue: An infinite loop occurred on leap years when the day was 366.

  • The root cause was the if statement without an else within the leap year check resulting in being unable to decrement days.

  • Microsoft's failure to catch the leap year bug highlights the challenges of thorough testing.

  • Incorrect fixes for the bug:

    • The initial fixes posted online were also incorrect, demonstrating the subtlety of the problem.
    • It took three attempts to produce a correct fix, highlighting the difficulty of ensuring correctness even in simple programs.

Timsort Bug

  • Timsort: A sorting algorithm used in Java's Collections.sort and Arrays.sort methods, and formerly in Python.
  • Developed in 2002 by Tim Peters, Timsort adapts to runs of already sorted data within the input.
  • Combines merge sort and insertion sort techniques for efficiency.
  • In 2015, a Dutch computer scientist discovered a bug in Timsort that could lead to an "ArrayIndexOutOfBoundsException".
  • The bug's existence despite extensive testing highlights the limitations of relying solely on testing for correctness.
  • The bug was identified through formal methods.

Formal Methods

  • Formal methods: Mathematical techniques for reasoning about programs and software.
  • Edsger Dijkstra's quote: "Program testing can be used to show the presence of bugs, but never to show their absence."
  • Formal methods aim to prove the absence of bugs by treating programs as mathematical objects.
  • Involves formal specification and formal proof to verify program correctness.
  • Formal methods are typically applied to critical or complex parts of code rather than entire large programs.
  • Early work in formal methods:
    • Robert Floyd (1967): Assigned meanings to programs using predicate logic.
    • Tony Hoare (1969): Developed an axiomatic basis for computer programming.
    • Edsger Dijkstra: Weakest precondition calculus.
  • Adoption by Industry:
    • Initially limited to safety-critical software (aerospace, railway).
    • Increased adoption in recent years by companies like Amazon and Meta.
  • Key factors driving adoption include:
    • Increased importance of verifying programs.
    • Development of powerful automated tools.
    • Examples of tools: Key, Verifast, Viper, Dafny.
    • Languages designed for verification: Y3, Whiley, Dafny.

Course Overview

  • Focuses on formal verification of program correctness.
  • Covers deriving correct programs from formal specifications.
  • Uses the Daphne tool for formal verification.

Daphne: A Verification-Aware Programming Language

  • Supports formal specifications and static program verification.
  • Object-based (classes and objects) but without inheritance.
  • Supports functional programming (not covered in this course).
  • Can be compiled to C, C++, Go, Java, JavaScript, and Python.
  • Daphne can detect runtime errors like division by zero and array index out of bounds.

Daphne Syntax Overview

  • Classes, functions, predicates, and methods.
  • Assignment (:=) including simultaneous assignments.
  • Variable introduction (var).
  • If-then-else statements and while loops.

Daphne Types

  • Native basic types: Booleans, characters, integers, naturals, reals.
  • Collection types: Sequences, sets, multisets, maps.
  • Arrays for efficient programming.

Zoom Bug Revisited using Daphne

  • The Zoom bug code rewritten in Daphne. Daphne immediately flags the non-termination issue.
  • Daphne indicates "cannot prove termination"
  • Daphne can detect possible division by zero errors with the message "possible division by zero"
  • Daphne can detect index out of range errors with the message "index out of range"