Explore

F23 Mad 5234 LA 5: Mathematical proofs of algorithm and program execution correctness.

DUE: May 23 11:59 p.m.

How to submit this work:

Lean into your Markdown and GitBook Skills.

Put your GitBook URL into a text file named as studentname_studentid.txt

(text file NOT Word!)

Upload to:

https://www.dropbox.com/request/UnlZ7pJbNBoeJykFo2ea⁠

⁠

Outline and description of a three-part lesson on mathematical proofs of algorithm and program execution correctness.

PART 1: Proving Algorithm Correctness:

In this part, students will learn about the basics of algorithm correctness.

They will learn how to use mathematical induction to prove the correctness of an algorithm.

Introduction to Algorithm Correctness:

Define what it means for an algorithm to be correct and the importance of proving algorithm correctness.

Mathematical Induction:

Explain the concept of mathematical induction and how it's used to verify a statement for every natural number.

Proving Algorithm Correctness with Induction:

Use examples to illustrate how to prove the correctness of an algorithm using mathematical induction.

Let's proceed with a specific example to better illustrate the given material.

PART 1: Proving Algorithm Correctness

QUICK OVERVIEW:

Introduction to Algorithm Correctness:

An algorithm is said to be correct if, for every input instance, it halts with the correct output.

Ensuring an algorithm's correctness is essential as it validates that the algorithm is accurately solving the intended problem.

Mathematical Induction:

Mathematical induction is a mathematical proof technique used to establish that a given statement is true for all natural numbers.

It consists of two steps:

The base step (proof of the statement for the first natural number)

and the inductive step (proof that, if the statement holds for some natural number, it holds for the next natural number as well).

Proving Algorithm Correctness with Induction:

Mathematical induction can be applied to verifying algorithm correctness.

Each step of the algorithm corresponds to an inductive step in the mathematical induction proof, confirming the algorithm is valid for all input instances.

APPLIED EXAMPLE: SUM OF NATURAL NUMBERS

Let’s take an example of an algorithm that calculates the sum of the first N natural numbers. The formula is:

Sum(N) = N * (N + 1) / 2

INTRO:

This simple algorithm is said to calculate the sum of the first N natural numbers.

We'll now attempt to prove its correctness.

ASSUMPTION - BASE CASE (for N=1):

First, we prove this formula works for N=1.

Sum(1) = 1 * (1 + 1) / 2 = 1, which is true, as the sum of the first 1 natural number(s) is indeed 1.

INDUCTIVE STEP:

Next, we make an inductive hypothesis.

We assume this formula works for some natural number k (that Sum(k) = k * (k + 1) / 2 is true), and we need to prove that the formula will then work for k + 1.

So we want to prove Sum(k + 1) = (k + 1) * ((k + 1) + 1) / 2. If we simplify this, we need to prove that

Sum(k + 1) = (k + 1) * (k + 2) / 2 = (k^2 + 3k + 2) / 2.

We also know that Sum(k + 1) = Sum(k) + (k + 1) based on the definition of the problem.

Substitute Sum(k) from our inductive hypothesis into this equation:

= (k * (k + 1) / 2) + (k + 1) = (k^2 + k + 2k + 2) / 2 = (k^2 + 3k + 2) / 2

Hence, we've successfully completed our inductive step and have shown that if our formula is true for some number k, then it's also true for k + 1.

CONCLUSION: What Induction means

Induction is our mathematical tool for proving algorithm correctness

Now, we've established the correctness of the algorithm using mathematical induction. It guarantees that no matter which number N we're finding the sum of, our algorithm will correctly calculate it. This is a typical example of using mathematical induction to verify correctness in algorithms.

The net sum of this is:

I have some code:

It should do one or the other of two things:

Your method should do either:

A. Excute its instruction AND pass the flow of control to the next program instruction frame - OR -

B. HALT.

PART 2: Proving Single Class Method Correctness:

This part focuses on proving the correctness of single class methods in a program.

Concepts like invariants and pre/post conditions are crucial here.

- Introduction to Class Methods:

Briefly review what a class and a method are and their roles in a program. Class Invariants and Method Specifications: Define what invariants, preconditions, and postconditions are in a class method.

Proving Method Correctness: Demonstrate how to prove the correctness of a method by ensuring that given the preconditions, the postconditions will always hold.

Let's dive deeper into proving single class method correctness with a Code Example.

PART 2: Proving Single Class Method Correctness

Let’s consider a basic class method: the `sum()` method from the ArrayIntList class in Java.

This method calculates the sum of all numbers in the list.

```java //ArrayIntList class would look some thing like this:

public class ArrayIntList { private int[] elementData; // list of integers private int size; // current number of elements in the list //Constructors and other methods would be here public int sum() { int output = 0; for (int i = 0; i < this.size; i++) { output += this.elementData[i]; } return output; } } ```

Our goal is to verify that the `sum()` method operates correctly - it accurately computes the sum of all integers in the ArrayIntList.

Introduction to Class Methods:

In a Class, methods are blocks of code that execute a specific task or algorithm.

Here the `sum()` method is used to calculate the sum of integers in an ArrayIntList.

Class Invariants and Method Specifications:

Preconditions:

What must be true before the method runs.

For our `sum()` function, the precondition is that the ArrayIntList must be initialized (not null).

Postconditions:

What will be true after the method completes.

For our `sum()` function, the postcondition is that the sum of all integers in the ArrayIntList is returned. Proving Method Correctness:

To prove the correctness of the `sum()` method, it must hold true that given preconditions (ArrayIntList is initialized), the postconditions (sum of integers in the ArrayIntList is returned) will always be satisfied.

If the ArrayIntList is initialized, the `sum()` method iterates through the array, summing up each element.

At the end of the iteration, it returns the total sum, satisfying the postcondition.

So the correct behavior of this method under specified conditions (pre/postconditions) confirms the correctness of this method.

This concept of ensuring pre/postconditions is a basic but fundamental principle in proving the correctness of program execution at the level of class methods.

Remember, for complex methods with intricate logic the process could be more complicated but the principles stay the same.

A simple Java code and a template of a worked-out example based on the this scenario:

Sample Java Code:

public class ArrayIntList {

private int[] elementData;

private int size;

// Constructor to initialize the array and size

public ArrayIntList(int[] input) {

this.elementData = input;

this.size = input.length;

}

// Sum method as described

public int sum() {

int output = 0;

for (int i = 0; i < this.size; i++) {

output += this.elementData[i];

}

return output;

}

// Main method to test our ArrayIntList class

public static void main(String[] args) {

int[] testData = {1, 2, 3, 4, 5};

ArrayIntList list = new ArrayIntList(testData);

System.out.println("Sum of integers in the ArrayIntList: " + list.sum()); // Expected output: 15

}

Worked Out Example:

Let's prove the correctness of the sum() method for the ArrayIntList class.

We'll follow a step-by-step approach:

Problem Statement:

We have an integer array called elementData. We want to calculate the sum of all elements present in this array.

Preconditions:

elementData should be initialized. (i.e., it should not be null)

size variable should accurately represent the number of elements in elementData.

Postconditions:

The method should return the correct sum of all integers present in elementData.

Approach:

Initialize an output variable to 0.

int output =0;

Iterate over elementData using a loop running from 0 to size - 1.

For each iteration, add the current element to the output.

Return output at the end.

Proof:

Given our preconditions, we are sure that our array is initialized and we know its size.

Now, during every iteration, we are simply adding the array's current element to our output. So, by the end of the loop, output will have the sum of all elements of elementData. Thus, our postcondition (method should return the correct sum) is satisfied.

Verification:

Using our sample data of {1, 2, 3, 4, 5}, we get an output of 15, which matches our expected output.

This confirms our method's correctness for this dataset.

While this is a simple example, the principle of ensuring pre/postconditions and then proving them holds true for more complex scenarios.

The key is breaking down the problem, identifying conditions, and then methodically proving them using the logic of your code.

What you are to do:

Assignment: Prove Method Correctness for a String Manipulation Class

In this assignment, students will dive deep into proving the correctness of class methods.

Using the principles learned from the ArrayIntList example, students will focus on a new class called StringManipulator.

Objective:

Create a StringManipulator class that has methods for string operations.

Prove the correctness of each method by specifying preconditions and postconditions and then validating them.

Task Description:

StringManipulator Class Creation:

Design a class called StringManipulator with the following methods:

reverse(): Returns the reversed version of the input string.

toUpperCase(): Converts and returns the string in uppercase.

concatenate(String str1, String str2): Returns the concatenated result of str1 and str2.

Preconditions and Postconditions:

For each method, note in your GITBOOK as much as you can think about for these issues:

Preconditions: What must be true before the method is executed.

Postconditions: What is expected to be true after the method is executed.

Prove Method Correctness:

For each method, provide a step-by-step breakdown similar to the ArrayIntList example.

Ensure that given the preconditions, the postconditions will always be satisfied.

Submission:

A StringManipulator.java file containing the class and methods. (already provided, below)

A ProofOfCorrectness.md file in markdown format, detailing:

The preconditions and postconditions for each method.

A step-by-step breakdown proving the correctness of each method.

Grading Rubric:

1. Code [40 points]

Proper class and method structure: 10 points

Code correctness for each method: 10 points each

2. Proof of Correctness Documentation [60 points]

Clearly defined preconditions and postconditions: 15 points

Detailed breakdown proving correctness for reverse(): 15 points

Detailed breakdown proving correctness for toUpperCase(): 15 points

Detailed breakdown proving correctness for concatenate(): 15 points

Additional Guidelines:

The strings you work with can consist only of alphabets (uppercase/lowercase) and spaces.

Make sure your methods handle edge cases: e.g., empty strings.

For the purpose of this assignment, you don't need to consider null strings.

Final Note:

Through this assignment, you will hone your skills in understanding how methods work and ensuring they operate correctly under defined conditions.

You will sensitive your Programmer’s Intuition as to how to formulate your methods to make them easily.

Note: Document your assumptions as you are writing your Code.

Always remember to break down your problems, and methodically prove them using the logic of your code.

Below is a fully worked out Java application for the StringManipulator class and a sample demonstration in the main method:

javaCopy code

public class StringManipulator {

// Constructor

public StringManipulator() {

}

// Returns the reversed version of the input string.

public String reverse(String input) {

// Ensure input is not null

if (input == null) {

return null;

}

Want to print your doc?
This is not the way.

Try clicking the ⋯ next to your doc name or using a keyboard shortcut (

CtrlP

) instead.