top of page

Week 3

The material of the third week goes over types and introduces Precondition and Postcondition.

Types and Variables

Expressions

An expression is either a value or a combination of operands and operators which produce a value of some type. The most simple expressions are literals which are values directly written into the program. Expressions can be nested, i.e. expressions can appear inside of expressions. This should not be surprising as we have seen this behaviour before with EBNF rules which themselves contain EBNF rules. A simplified EBNF rule definition for <expression> can be found below.

<number> <= <integer> | <digit> {<digit>} . <digit> {<digit>}
<op> <= + | - | * | / | %
<atom> <= <number> | <identifier>
<term> <= "(" <expr> ")"  |  <atom>
<expr> <= <term> { <op>  <term>}

Types and Variables

Variable

typename variableName = value;

A variable is used to store data which we want to refer to at a later point in the program. A variable has a name, a type and a value (if it was assigned one). We will learn later on how the type of a variable restricts the type of data which can be stored in a variable. Variables are used everywhere and hence it is important that one chooses a name that is descriptive in regards of the data that the variable carries. Variable naming is one of the most important aspects of writing readable code. 

Types and Variables

Java Types

In this section we will quickly look at the most important types in Java. All types discussed here besides Strings are primitive types. What this exactly means will be discussed later on.

int age = 22;

The int type in Java represent integers. It can store any integer and has a range of 32bits, i.e. it can store represent a total number of 2^32 distinct integers. This includes positive and negative number, hence approximately half of the representable numbers are positive and half are negative (zero is neither). We hence expect that the largest number a variable of int can be assigned to must have an absolute value somewhere close to 2^31. Once can use Integer.MAX_VALUE and Integer.MIN_VALUE to verify this for themselves. The long type is a 64bit version of the int type and also exists in Java.

double balance = -121.25

The double type in Java represent real numbers. It can only represent a real number to a certain accuracy and it is a 64bit type. How (double) floating point numbers work is not of concern right now and will be discussed in detail in future lectures. Alternatively one can also make usage of the float type which is the same as double but is a 32bit type. Floats will not appear in this lecture as any time we want to store real numbers we use the double type.

char surnameInitial = 'z';

The char type in Java is used to store ASCII characters. We put any (printable) ASCII characters in between single quotation marks when assigning a char type variable a char value. It is important to note the difference between 'z' and "z" as one is a char and the other is a length one string.

boolean opened = false;

The boolean type in Java is used to store a single bit of information. It also supports logical operations which we will see later on. We can assign to any boolean type variable only the values true and false.

String name = "Cédric"

The String type is not a primitive type. It is a sequence of characters and there exists a String class which is the reason why we can call functions on any String object. We cannot do the same with primitive types. This is a very important difference.

Types and Variables

Operators + -

Addition and Subtraction

Addition and subtraction are given in Java by the operators + and - respectively. We can apply addition and subtraction to all primitive types besides boolean type values and variables. For all numerical types addition and subtraction does what we would expect. When adding or subtracting floating point numbers (double / float) one may observe inaccuracies in the result somewhere after the tenth digit. This comes as a consequence of the mentioned limited accuracy of floating point numbers and is not a concern for most computations. Overflow occurs with all types besides floating point numbers. Floating point numbers do not overflow, instead they are set to Infinity. This is not important in the context of this lecture.

+ and - with char

We have seen how any (printable) ASCII character can be stored in a char type variable. This however is not the entire truth, we can in fact store any number between 0 and 65535 in a char type variable. 65535 is one less than 2^16 which makes sense, because the char type is a 16 bit type. This comes because char type variables use Unicode and not ASCII to represent its characters. The first 128 characters of Unicode and ASCII are the same however which is why one uses the ASCII table to translate between the most common characters and its number representation. The character with number 2023 is given by ߧ for example. Adding and subtracting char type values and variables is done by first translating the characters into their Unicode number and the doing integer addition and subtraction.

+ with String

For Strings only addition is defined. Adding two Strings will concatenate them. Concatenation is the process of combining two strings by putting the second one right after the first one, e.g. concatenating "Hello" and "Alice" will yield "HelloAlice". Concatenation is important when printing output as it allows us to take user input and add it to the output. An example of this can be seen below.

Concatenate.png

Types and Variables

Operator * / %

Multiplication

Multiplications in Java is given by the operator * and can be applied to all primitive types besides boolean type values and variables. Overflow again occurs with all types besides floating point numbers. With chars we again first convert the characters into their numerical Unicode representation and then multiply these numbers.

Division

Division in Java is given by the operator / and can be applied to all primitive types besides boolean type values and variables. Division on floating point numbers (besides the inaccuracy aspect) works as expected. Integer division or division on any other non-floating point primitive type works differently. Dividing 3 / 2 one would expect 1.5 to be the result. However we want the result of two integers being divided to be an integer. Hence integer division works by rounding down any result to the nearest integer. Hence we have 3 / 2 = 1. One must remember this as it is one of the things often forgotten in programming which leads to error in the code or to wrong answers on theory questions. Integer division produces an error if one attempts to divide by zero.

Modulo

Modulo is given by the operator % and can be applied to all primitive types besides boolean type values and variables. Modulo works by taking the greatest multiple of the Divisor such that it is still smaller than the Dividend. If you do not quite remember which one is which (neither did I) we have Quotient = Divisor / Dividend. The remaining difference between this greatest multiple and the Divisor is then the result of the modulo operation. This is division with remainder which you all should have seen at some point during your school career. In Java for negative operands (first operand) we will also get a negative result, remember this.

Types and Variables

Operator Evaluation

     4 + 3 * 2 / 2 % 9    
=  4 + (3 * 2) / 2 % 9
=  4 + ((3 * 2) / 2) % 9
=  4 + (((3 * 2) / 2) % 9) 
=  4 + ((6 / 2) % 9)
=  4 + (3 % 9)
=  4 + 3
=  7

Given an expression with multiple operators and no parentheses we must have a set of rules telling us in what order operators are executed. For this purpose we use the same precedence rules as in mathematics. Expressions in parentheses are evaluated first, then we evaluate multiplicative operations like multiplication, division and modulo, and at last we evaluate additive operations like addition and subtraction. We will see many more operators in the following chapters, however now we will focus on arithmetic operators. If the operator precedence is equal between two operations we evaluate from left to right with arithmetic operations.

Types and Variables

Operator Associativity

a ⊗ b ⊗ c = (a ⊗ b) ⊗ c

a ⊗ b ⊗ c = a ⊗ (b ⊗ c)

Operators can associate to the right or to the left. We are used to operators associating to the right, i.e. multiple operations being evaluated from left to right. There are however operator which we will see later on that associate to the right. In the example to the left the top operation evaluation shows left associativity and the bottom operations shows right associativity.

Types and Variables

Implicit Casting

byte -> short -> char -> int -> long -> float -> double

Given an expression with mixed (primitive) types we must also have a set of rules that tells us what the type of the result will be. In Java any primitive types differ simply by the size and how the data is to be interpreted. We can hence store a smaller number stored in an int type variable directly in a long type variable. The same is true for all primitive types besides the boolean type. To the left one can see what types can directly be assigned to each other without having to manually do anything. We call this behaviour implicit casting as the type conversion is done for us automatically.

Types and Variables

Direct Casting

double -> float -> long -> int -> char -> short -> byte

long l = 2024L;
int i = (int) l;

There is also the possibility to convert from a larger primitive type to a smaller primitive type with a potential lossy conversion by using a (direct) type case. This is done every time we want to manually force a primitive type to be casted into another primitive type. If a long type variable stores a larger number than an integer can fit only half the bits will be considered which will produce a completely different number. Hence we do this only when we know that it makes sense to do so and will not result in a loss of data.

To the left one can see the syntax for casting. The addition of the L to the number is something one should remember as all numerical values typed into code will be interpreted as int type value and hence we cannot assign number larger than 2^32 to long type variable if we do not add the L behind the numerical value to make sure that the value is recognised as a long value and not an int value. The cast operator is an example of a right associative operator as multiple casts without parentheses are evaluated right to left.

Types and Variables

Logical Operators

true || true   -> true
true || false  -> true
false || true  -> true
false || false -> false

true && true   -> true
true && false  -> false
false && true  -> false
false && false -> false

!true -> false
!false -> true

We have discussed arithmetic operators that can be applied to all types but the boolean type. We now discuss logical operators. Logical operators can be applied to boolean type values and variables and to no other types. In the discrete mathematics lecture you should have seen the logical operators ∧, ∨, ¬, which are conjunction, disjunction and negation respectively. In Java these operators exist in the form of logical AND &&, logical OR | | and logical negation ! which work exactly as their counterparts in mathematics.

Logical operators are used in almost any Java program and you will see them in all parts of the lecture, it hence is advised to understand very well how to work with them. One thing that is used many times is short circuiting. Short circuiting works by evaluating only parts of a logical expression involving | | or &&. If the first operand of an operation involving | | evaluates to true Java will not evaluate the second operand and the entire operation will evaluate to true. The same is true for && but if the first operand evaluates to false, and the operation will then evaluate to false.

Types and Variables

Relational Operators

true == true -> true
1 == 2 -> false
'a' ==  97 -> true

2 < 2 -> false
2 <= 2 -> true
2 != 2 -> false
2 == 2 -> true

Another important set of operators is given by relational operators which are used to compare two given values. The first and most important relational operator is given by the equality operator ==. This operator works on all primitives types and can be applied to two variables or values of the same type or alternatively, if one of the types can be implicitely casted to the other, of different type. We will later see that that this extends to non-primitive types but that there we must be a bit more careful as the equality operator works differently there.

In addition to equality we can also compare greater than, smaller than with > and < respectively and in addition to that we can also compare greater or equal and smaller or equal using >= and <=.

Although not strictly necessary we can use the != operator to check if two values or variables are not equal to each other.

Precondition and Postcondition

Make Statements about a given Program

Forward reasoning

Backwards reasoning

We have seen already very simple Java programs and might now ask the question how to verify whether or not a given such Java program is logically correct or not. Program verification is a very complex topic that extends far beyond the scope of this lecture. We will however cover basic program verification tools which we will use to make statements on the state of certain variables after execution of small programs.

We start of by observing that given a list of statements to be executed one after the other and we state the initial state of all involved variables we may make a statement on the state of said variables after the execution of all or some of the statements. This initial state is what we call the precondition.

We can alternatively also state the state of the the variables at the end of the execution of all or some statements. This is then referred to as the postcondition. We then argue backwards and attempt to reconstruct the initial state of said variables using the statements involved.

Precondition and Postcondition

Forwards Reasoning

// w > 0
x = 17;
//
y = 42;
//
z = w + x + y;
//

// w > 0
x = 17;
// w > 0 
 x == 17

y = 42;
// w > 0 
 x == 17   y == 42
z = w + x + y;
// w > 0 
 x == 17
   y == 42   z > 59 

Forward reasoning works by looking at the given precondition and then go over every statement in the order of execution one by one and observe how it affects the variables in the precondition and adding any conditions newly introduced on different variables as well. In the code to the left we are given the precondition w > 0.

Executing x = 17 does not affect the variable w but it introduces a new condition on the newly introduced variable x hence we can construct the new list of conditions as w > 0 and x == 17. We use ∧ instead of the word "and" in listing the conditions which is the logical conjunction symbol you should be familiar with from the discrete mathematics lecture.

In a next step we have he statement y = 42 which again introduces a new condition which we will simply add to the list of current conditions.

At last we have the statement z = w + x + y. What we do now is to replace x and y by their value we can follow from the list of conditions, we then replace w by 0 and replace = with > as this is the strongest statement we can make. We then add this to the list of conditions we have gathered over the execution of all statements.

Precondition and Postcondition

Backwards Reasoning

// 
x = 17;
//
y = 42;
//
z = w + x + y;
// z < 0

// w < -59 
x = 17;
// w + x + 42 < 0 

y = 42;
// w + x + y < 0

z = w + x + y;
// z < 0

Backwards reasoning works very similar to forwards reasoning by making a statement on the initial state of variables given their state at some point of the execution of given statements. In the example to the left we start of with z < 0 and then can see that the previous statement set z to the value of w + x + y and hence we conclude that w + x + y < 0.

 

The next statement is y = 42, we can hence substitute y in the condition w + x + y < 0 by its value giving w + x + 42 < 0. One cannot add y == 42 to the conditions since it is set only afterwards, this is often added by mistake and the leads to errors.

We now do the same with x = 17 which yields w + 59 < 0 which is equivalent to w < -59. It is important to again remember that we cannot add the condition x == 17. The backwards reasoning attempts to make a statement on the variable w and not x and y which values are known at the end of executing the instructions.

Backwards reasoning is more often used when programming as we often have the results of our program and are trying to figure out what went wrong.

Precondition and Postcondition

Syntax

// x < 0 && y == 2
// x < 0 
 y == 2
{ x < 0 && y == 2}
{ x < 0 
 y == 2 }

We use a combination of Java syntax and boolean logic operators for pre- and postconditions. Instead of writing x = 18 you should write x == 18. You may use the Java logical operators && and | | instead of their boolean logic counterparts ∧, ∨. What one cannot do is introduce Java statements which have an effect on the variables involved. An example for this would be x = y + 1 or x = x + 1. This is the reason why you should always use the equality operator == in pre- and postconditions and not the equal = symbol as it could be misunderstood as assigning a value to a variable.

In some sources online you might find pre- and postconditions wrapped in curly brackets {  and } instead of using the // comment notation we use here. 

Precondition and Postcondition

Implement in Java

AssertExample.png
AssertionsFailing.png

There is no direct support for pre- and postconditions in Java. One can however make use of the assert statement. One takes a condition and puts it after the assert statement. This will then only allow for the statement after the assert statement to be executed if the given condition holds, else execution will stop and the program will produce an error.

Assertions are disabled by default and one must pass the -ea flag as a VM argument to enable them. It must also be said that using assert in general should not be done for any purpose besides debugging.

In the code to the left the last line will not be executed, i.e. "I was executed" will no be printed due to the assertion failing.

Hoare Triple

Implement in Java

{ P }  S  { Q }

We can combine pre- and postconditions into one construct. This is done by having a precondition P and a postcondition Q before and after some statement S. This triple we refer to as a Hoare Triple. A Hoare triple is valid if and only if the following condition holds

For any initial state if the condition in the precondition P is satisfied before the execution of the statement S, then after the execution of S the postcondition Q must be satisfied.

That is it.

You are done with theory. To make sure you understand the theory you need to apply what you learnt in practice. Solve the exercises.

bottom of page