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:
- Understand the Postcondition: Begin by precisely defining what the loop should achieve. What must be true after the loop completes? This is your postcondition.
- 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.
- 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.
- 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.
- 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.
- 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
.
-
Postcondition: After the loop,
max
should hold the largest value present in theitems
array. -
Invariant (Initial Hypothesis):
max
stores the maximum value encountered so far in the array up to indexi-1
, and0 < i <= length
, wherelength
isitems.length
. -
Loop Body (Preserving the Invariant):
-
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: Wheni == items.length
, the invariant states thatmax
holds the maximum value up toitems[length - 1]
, which is the maximum of the entire array. -
Initialization (Establishing the Invariant): To establish the invariant before the loop, we initialize
max
to the first element of the array andi
to 1:max = items[0]; i = 1;
-
Final Code:
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:
- State: The module should be able to store and manage its internal data.
- Behavior/Functionality: The module should provide methods for interacting with and manipulating its state.
- 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
- Uniformity: All points should have the same structure: an x-coordinate and a y-coordinate.
- Distinct Instances: Different instances (objects) of the
Point
class can have different x and y values. - Multiple Instances: We should be able to create as many
Point
objects as needed. - Output: We should be able to display the coordinates of a point (we’ll cover this later).
- 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:
Example: Point Class
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:
Example:
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
: 0double
: 0.0boolean
: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:
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:
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:
Continue here: 12 Null, Class Methods, Constructors