11 Loop Invariants, Classes and Objects, Attributes, Reference Semantics

Lecture from: 29.10.2024 | Video: Videos ETHZ

Loop Invariants

The previously mentioned strategy for developing loops with invariants is a good starting point. However, finding invariants and developing correct loops is often an iterative process. Here’s a more general strategy emphasizing this iterative and often non-linear nature:

1. Understand the Postcondition: Begin by precisely defining what the loop should achieve. What must be true after the loop completes? This is your postcondition.
2. Hypothesize an Invariant: Formulate a potential invariant. A good invariant is a property that:
   • Holds before the loop starts.
   • Remains true before and after each iteration.
   • When combined with the negation of the loop condition, implies the postcondition.
3. Develop the Loop Body (Invariant Preservation): Write the code inside the loop, focusing on maintaining the invariant. If the invariant holds true before an iteration, it must still be true after the iteration.
4. Refine the Loop Condition (Towards Termination and Postcondition): Design or refine the loop condition. The condition should:
   • Ensure the loop eventually terminates.
   • When combined with the invariant, logically imply the postcondition.
5. Establish the Invariant (Initialization): Write the code before the loop to initialize variables and establish the invariant, making sure it’s true even before the first iteration.
6. Iterate and Refine: This is crucial. Loop development is rarely a linear process. You’ll likely need to:
   • Revise your invariant if it’s too weak to prove the postcondition or too strong to be easily established.
   • Adjust the loop body to preserve a revised invariant.
   • Modify the loop condition to ensure termination and correct postcondition establishment.
   • Change the initialization code to establish a revised invariant. Be prepared to cycle through steps 2-5 multiple times until you have a correct and verifiable loop.

Example: Finding the Maximum Element in an Array

Let’s apply this general strategy to a classic problem: finding the maximum element in an array.

Goal: Find the maximum value max in a non-empty array int[] items.

1. Postcondition: After the loop, max should hold the largest value present in the items array.

2. Invariant (Initial Hypothesis): max stores the maximum value encountered so far in the array up to index i-1, and 0 < i <= length, where length is items.length.

3. Loop Body (Preserving the Invariant):

if (max < items[i]) {
	max = items[i]; // Update max if a larger element is found
}
i = i + 1; // Move to the next element

4. Loop Condition (Termination and Postcondition): The loop should terminate when we’ve examined all elements. So, the condition is i != items.length. Together with the invariant, this implies the postcondition: When i == items.length, the invariant states that max holds the maximum value up to items[length - 1], which is the maximum of the entire array.

5. Initialization (Establishing the Invariant): To establish the invariant before the loop, we initialize max to the first element of the array and i to 1: max = items[0]; i = 1;

6. Final Code:

{items != null ∧ items.length > 0} // Precondition: Non-null, non-empty array
int max = items[0];
int i = 1;
{inv: (max is the maximum of items[0]...items[i-1]) ∧ (0 < i ≤ items.length)}
while (i != items.length) {
	if (max < items[i]) {
		max = items[i];
	}
	i = i + 1;
}
{(max is the maximum of items[0]...items[items.length-1])} // Postcondition

Classes and Objects

This lecture introduces the concepts of classes and objects in Java, which are fundamental to object-oriented programming (OOP). We’ll explore the motivations behind using classes, their core components (attributes and methods), and how they facilitate modular and maintainable software development.

Motivation: Software Development at Scale

Large programs are typically composed of individual modules. These modules can vary significantly in size and functionality, ranging from large, standalone applications (like a database) to small libraries providing specific utilities (like java.util.Random). In object-oriented languages, classes are the primary tool for building these modules.

Classes offer a way to encapsulate related data (state) and the operations that act on that data (behavior). This encapsulation promotes modularity and makes it easier to manage complex software projects.

Requirements for Modules

A good software module should address the following aspects:

1. State: The module should be able to store and manage its internal data.
2. Behavior/Functionality: The module should provide methods for interacting with and manipulating its state.
3. Lifecycle: The module should define how its instances (objects) are created, used, and eventually destroyed.

Example: Toggle Switch

Consider a toggle switch in a graphical user interface (GUI) library.

• State: The switch can be either “on” or “off,” and it might have properties like color, size, etc.
• Functionality: Provides operations like turnOn(), turnOff(), isOn(), etc.
• Lifecycle: Instances of the toggle switch are created and added to the GUI, manipulated by the user, and eventually removed when no longer needed.

Classes provide the structure to define and manage these aspects of a module effectively.

From Arrays to Classes

We’ve already worked with arrays, which can store data (representing state). However, arrays have limitations:

• Data Organization: Arrays are simple containers. They don’t provide a way to group related data elements together naturally. If we need to represent something with multiple properties (like a person with a name, age, and email address), we’d need separate arrays for each property, making the code harder to manage and understand.
• Limited Functionality: Arrays only offer basic operations for accessing and modifying elements. They don’t provide a mechanism for defining custom operations related to the data they store.

Motivating Example: Sports Data Analysis

Suppose you want to analyze sports data, including the average height of athletes and the number of athletes above the average height. You now need to email this analysis to each athlete, requiring you to store their email addresses along with their heights. Using arrays, you’d need separate arrays for height and email, creating a potential for inconsistencies and making it difficult to manage the data if you want to sort or filter it.

Classes to the Rescue

Classes address these limitations by bundling data and related operations into a single unit. In the sports data example, you could create a Person class to store each athlete’s height, email, and other relevant information. The class could also provide methods for calculating the average height, filtering athletes, and generating email reports.

Object-Oriented Programming (OOP)

Object-oriented programming (OOP) is a programming paradigm that organizes a program as a collection of interacting objects. Each object has:

• State (Attributes): Data associated with the object.
• Behavior (Methods): Operations the object can perform.

Objects interact by calling each other’s methods, and the overall program behavior emerges from these interactions.

Java and OOP

Java is an object-oriented language, meaning classes are the core building blocks of Java programs.

Representing Points in 2D Space

Let’s illustrate the concepts of classes and objects with a concrete example: representing points in a 2D plane.

Requirements

1. Uniformity: All points should have the same structure: an x-coordinate and a y-coordinate.
2. Distinct Instances: Different instances (objects) of the Point class can have different x and y values.
3. Multiple Instances: We should be able to create as many Point objects as needed.
4. Output: We should be able to display the coordinates of a point (we’ll cover this later).
5. Equality: We should be able to check if two points are equal (also covered later).

Defining Classes and Attributes

In Java, a class is defined using the class keyword, followed by the class name and a block of code enclosed in curly braces {}. Inside this block, we declare the attributes and methods of the class.

Syntax:

// In file Name.java  (Filename must match class name)
public class Name {
    type1 attribute1;
    type2 attribute2;
    // ... more attributes
    // ... methods (will be covered later)
}

Example: Point Class

public class Point {
    int x;
    int y;
}

This code declares a class named Point with two attributes: x and y, both of type int. These attributes represent the coordinates of a point.

Attributes (Fields, Member Variables, Object Variables, Properties)

Attributes store the data associated with an object. Each object of a class has its own set of attribute values. The combination of attribute values determines the state of an object.

Creating Objects (Instantiation)

Objects are created using the new operator, followed by the class name and parentheses (). This process is called instantiation. The new operator allocates memory for the object and initializes its attributes to default values.

Syntax:

Name objectReference = new Name(); 

Example:

Point p1 = new Point();
Point p2 = new Point();

This code creates two Point objects. p1 and p2 are references to these objects. Because no explicit values were provided during instantiation, the x and y attributes of both p1 and p2 are initialized to 0 (the default value for int).

Generalization:

• A class acts as a blueprint or template for creating objects.
• Objects are instances of a class.
• The new keyword is used to create new instances. It returns a reference to the newly created object.

Default Attribute Initialization

When an object is created using new, its attributes are automatically initialized to default values:

• int: 0
• double: 0.0
• boolean: false
• Reference types (arrays, strings, other objects): null

Accessing and Modifying Attributes (Dot Notation)

We access and modify attributes using the dot notation (.).

• Reading: objectReference.attributeName
• Writing: objectReference.attributeName = expression;

Example:

Point p1 = new Point();
p1.x = 1;  // Set x-coordinate of p1 to 1
p1.y = 2;  // Set y-coordinate of p1 to 2
 
Point p2 = new Point();
p2.x = p1.y * 2; // Set x-coordinate of p2 to 4 (2 * 2)
 
System.out.println("p2.y = " + p2.y); // Output: p2.y = 0 (default value)

Reference Semantics

Variables that hold objects (like p1 and p2 in the Point example) actually store references to the objects, not the objects themselves. This is called reference semantics. It has important implications for how assignments and method calls work.

Assignment

Assigning one object variable to another copies the reference, not the object itself. This creates an alias: both variables now refer to the same object.

Example:

Point p1 = new Point();
p1.x = 11;
 
Point p2 = new Point();
p2.y = 22;
 
Point p3 = p2;   // p3 now refers to the same object as p2
p3.x = 33;      // Modifying p3 also modifies p2
 
p2 = p1;       // p2 now refers to the same object as p1
p2.y = -22;   // Modifies p1.y
 
// Now: p1.x = 11, p1.y = -22
//      p2.x = 11, p2.y = -22
//      p3.x = 33, p3.y = 22

Methods and References (Brief Introduction – More Later)

Objects are also passed to methods by reference. This means that a method can modify the state of the object passed to it.

Example:

void copyAndInc(Point src, Point dst) {
    dst.x = src.x + 1;
    dst.y = src.y + 1;
}
 
 
Point p1 = new Point();
p1.x = 10;
p1.y = 20;
 
Point p2 = new Point(); 
 
copyAndInc(p1, p2); // Modifies p2
 
// Now: p1.x = 10, p1.y = 20
//      p2.x = 11, p2.y = 21

Continue here: 12 Null, Class Methods, Constructors