The methods of the previous chapter are suitable for verifying systems of communicating processes, where control is the main issue, but there are no complex data. We relied on the fact that those (abstracted) systems are in a finite state. These assumptions are not valid for sequential programs running on a single processor, the topic of this chapter. In those cases, the programs may manipulate non-trivial data and – once we admit variables of type integer, list, or tree – we are in the domain of machines with infinite state space.

In terms of the classification of verification methods given at the beginning of the last chapter, the methods of this chapter are

1. Proof-based. We do not exhaustively check every state that the system can get in to, as one does with model checking; this would be impossible, given that program variables can have infinitely many interacting values. Instead, we construct a proof that the system satisfies the property at hand, using a proof calculus. This is analogous to the situation in Chapter 2, where using a suitable proof calculus avoided the problem of having to check infinitely many models of a set of predicate logic formulas in order to establish the validity of a sequent.

2. Semi-automatic. Although many of the steps involved in proving that a program satisfies its specification are mechanical, there are some steps that involve some intelligence and that cannot be carried out algorithmically by a computer. As we will see, there are often good heuristics to help the programmer complete these tasks. This contrasts with the situation of the last chapter, which was fully automatic.

3. […]

Motivation for verification

There is a great advantage in being able to verify the correctness of computer systems, whether they are hardware, software, or a combination. This is most obvious in the case of safety-critical systems, but also applies to those that are commercially critical, such as mass-produced chips, mission critical, etc. Formal verification methods have quite recently become usable by industry and there is a growing demand for professionals able to apply them. In this chapter, and the next one, we examine two applications of logics to the question of verifying the correctness of computer systems, or programs.

Formal verification techniques can be thought of as comprising three parts:

• a framework for modelling systems, typically a description language of some sort;

• a specification language for describing the properties to be verified;

• a verification method to establish whether the description of a system satisfies the specification.

Approaches to verification can be classified according to the following criteria:

1. Proof-based vs. model-based. In a proof-based approach, the system description is a set of formulas Γ (in a suitable logic) and the specification is another formula ϕ. The verification method consists of trying to find a proof that Γ ⊢ ϕ. This typically requires guidance and expertise from the user.

2. […]

The aim of logic in computer science is to develop languages to model the situations we encounter as computer science professionals, in such a way that we can reason about them formally. Reasoning about situations means constructing arguments about them; we want to do this formally, so that the arguments are valid and can be defended rigorously, or executed on a machine.

Consider the following argument:

Example 1.1 If the train arrives late and there are no taxis at the station, then John is late for his meeting. John is not late for his meeting. The train did arrive late. Therefore, there were taxis at the station.

Intuitively, the argument is valid, since if we put the first sentence and the third sentence together, they tell us that if there are no taxis, then John will be late. The second sentence tells us that he was not late, so it must be the case that there were taxis.

Much of this book will be concerned with arguments that have this structure, namely, that consist of a number of sentences followed by the word ‘therefore’ and then another sentence. The argument is valid if the sentence after the ‘therefore’ logically follows from the sentences before it. Exactly what we mean by ‘follows from’ is the subject of this chapter and the next one.

A structure is a user-defined data type that allows a single variable to store more than one type of data. In Visual Basic 6, structures were actually called user-defined types. The structure object has been improved in VB.NET, however, because VB.NET structures can contain both data and subprocedures to operate on those data. Structures are very common in form to classes, though they have several limitations that restrict their use to solve object-oriented programming problems. Because they are similar in form to classes, structures provide an excellent introduction to the use of classes, which is why we spend an entire chapter discussing them.

USING STRUCTURES

In Chapter 2 you were introduced to the concept of the abstract data type. To implement an ADT in VB.NET, we need to use a special data type called a structure. A structure allows us to store multiple components of different data types in one logical unit. In some languages structures are known as records.

The atomic data types (Integer, Single, String) allow us to store only single data items in a variable, as does an array (well, not strictly, since an array can be of type Object). For example, when we store a number in an Integer variable, we can only store one number in the variable. With structures, we can store more than one piece of the data in the structure and the data can be of different types.

Object-oriented programming (OOP) is just one in a series of technologies that has been deemed as the savior of software. In the world of computing, software often gets a bad reputation because so many programs are delivered to the end user late, with significant bugs, and not designed to completely solve the problem the program was written to solve. Object-oriented programming provides a set of tools and techniques to help programmers manage program complexity.

OOP DEFINED

Object-oriented programming is a programming technique that involves structuring a program around special, user-defined data types called classes. Classes are used to break a problem up into a set of objects that interact with each other. A class consists of both the data that define an object and subprograms, called methods, which describe the object's behavior.

A language that is to be called a true OOP language must implement three concepts—encapsulation, polymorphism, and inheritance. Without all three of these features, a programming language can be considered object-based, as Visual Basic 6 is, but all three must be present for the language to be considered a true object-oriented language.

Encapsulation

In the traditional, third-generation programming language (such as earlier versions of Basic, C, and Fortran), all programs consist of two primary elements—program statements and data. The program statements are used to perform operations on the data, but the two elements are always considered to be separate parts of a computer program.

This chapter explains how to perform database programming in an object-oriented way. There are several techniques (patterns) we can use to make a VB.NET/ADO.NET program object-oriented. Many of these techniques were first discussed (though not necessarily first used) in Martin Fowler's book Patterns of Enterprise Application Architecture (Fowler 2003). This chapter will distill some of the patterns he presents into working code that a VB.NET programmer will recognize, especially a programmer who now understands OOP. First, though, we'll provide you with an overview of how to use ADO.NET to access data stored in a database.

AN OVERVIEW OF ADO.NET

ActiveX Data Objects.NET (ADO.NET) is an object-oriented database API that allows a programmer to use one set of classes to access many different types of databases.

ADO.NET Objects

ADO.NET consists of a set of classes that encapsulate the behavior of the different aspects of a database. These classes include objects that represent the database, individual tables, columns within tables, and rows in tables. There are also specialized objects for making database connections and database commands.

The following list highlights these objects

• DataSet represents a subset of a database and is a parent object to many of the other objects used in ADO.NET.

• DataTable is used to work with the contents of a single table.

• DataColumn is used to represent each column in a table.

• DataRow represents a row of data from a table. Row data are retrieved from the Rows collection of a DataTable object.

• DataAdapter is used as a bridge between a DataTable object and the physical data source, or database, the program is using.

• […]

Programs written in VB.NET utilize the Throw-Catch model of exception handling when dealing with errors. The classes found in the.NET Framework use this model for handling errors, but the classes you develop must generate their own exceptions for handling errors. In this chapter, we discuss how exception classes are created and how to use them. We start the chapter with a review of the Throw-Catch model, which includes the Try-Catch-Finally statement.

EXCEPTION HANDLING IN VB.NET

The term VB.NET uses for errors that occur in executing code is exception. Writing code that deals with errors in a program is called exception handling. Exception handling in VB.NET consists of writing code that watches for exceptions when they're thrown and writing code that causes an exception to be thrown when an error condition arises. A VB.NET programmer is not responsible for always writing exception-generating code since the.NET Framework classes throw their own exceptions.

For example, trying to open a file that doesn't exist throws an exception because there was no file to open. This object is called FileNotFoundException. In the next section we examine how to write code to catch built-in exception objects.

Writing Exception-Handling Code

As we've discussed, trying to open a nonexistent file throws an exception. For our program to recognize the exception, we have to use a special construct—the Try-Catch-Finally statement.

Data we create via object creation cannot be treated in the same way native data (integers, strings, etc.) are treated. When we are working with strings, for example, it is easy to compare two strings to see if they are equivalent. In contrast, when we are working with two class objects, where each object is a composite of multiple data types, how we report the result of comparing the two objects is not obvious. Visual Basic.NET provides a special interface, IComparable, to aid us in making these types of comparisons.

Class objects also present a problem when we want to store them in a data structure and retrieve them using a For Each loop. The VB.NET compiler cannot automatically return an enumerator for class objects stored in an ArrayList or some other data structure, so we must provide the enumeration code. The.NET Framework again helps us in this task by providing an interface, IEnumerable, that we can implement. In this chapter we'll discuss how to implement both interfaces and provide several examples to see exactly how they're used.

THE ICOMPARABLE INTERFACE

A class type usually represents a complex data type comprising components of one of the built-in data types (String, Integer, Boolean, etc.). For example, an Employee class might include data for an employee's name (including the first, middle, and last name), social security number, salary, the department in which he or she works, etc. If we want to compare two Employee objects to see if they are the same, how do we do it?

It is not enough just to know how to write object-oriented programs; you also have to know how to write object-oriented programs well. As you gain experience writing object-oriented programs, you will discover certain programming idioms that are used over and over again. These idioms are called design patterns.

DESIGN PATTERNS

Design patterns were first described in Design Patterns—Elements of Reusable Object-Oriented Software (Gamma 1995). A design pattern is a solution to a recurring problem in object-oriented design and implementation. There are four parts to a design pattern, as described in Gamma et al.'s book (Gamma 1995, p. 3):

• Pattern name—A name for making it easier to discuss using the pattern.

• Problem—An explanation of the problem and its context.

• Solution—An abstract description of the design problem and how to use VB.NET code to solve it.

• Consequences—The pros and cons of implementing the design pattern.

The Shared Factory Method

Using constructors to create instances of classes is not always the preferred approach to instantiating class objects. One problem with constructors is that they don't have names, which can lead to confusing code. Another problem with constructors is that each constructor has to have its own signature, meaning that only one type of class object can be instantiated for each signature.

We can work around these problems by writing methods that create objects. This is a design pattern known as a factory method. In this case, we create a Shared Factory method that can be called without needing an instance of a class.

This chapter introduces the class, the primary means of implementing OOP in VB.NET. The class framework provides the programmer with many techniques for exploiting the three main principles of OOP—encapsulation, inheritance, and polymorphism.

Classes are somewhat similar to structures in that they allow you to combine data members and methods in the same unit. Classes, though, are much more powerful than structures because they have many more tools available to them. These tools include constructor methods for creating new objects and the capabilities of having multiple methods with the same name and inheriting the definition of one class in another class.

This chapter begins with an overview of class construction, followed by the step-by-step creation of a class, and finally ending with several more examples of creating and using classes. The next few chapters in the book will explore many of the topics we introduce in this chapter.

BUILDING A CLASS

Class construction follows naturally from a well-designed ADT. There are some modifications we'll have to make to our ADT design to incorporate some concepts found in classes but not in structures. Still, a complete ADT makes building a class much easier than if you start from scratch.

The Class Heading

Like a structure, a class definition begins with its heading. The heading of a class consists of an access modifier, the reserved word Class, and a name for the class.

Visual Basic is arguably the most popular application development programming language in use today. Thousands, if not millions, of programmers use it every day to build both commercial and scientific applications. The language is also one of the most maligned programming languages, second perhaps only to Cobol.

The newest version of Visual Basic, Visual Basic.NET (VB.NET), should eventually quiet many of those who call Visual Basic a toy language. Microsoft performed a major redesign of Visual Basic and added many features that put the language on equal footing with the other major.NET language, C#, and with other contemporary languages, especially Java.

One area of the language that has seen significant improvement is VB.NET's object-oriented programming features. In previous versions of Visual Basic, many of these features were partially implemented, not implemented at all, or implemented in a wrong-headed manner. VB.NET provides the programmer with a complete set of object-oriented tools. This book explains in detail how to use these features.

The book is informally partitioned into three parts. Chapters 1 through 6 present the fundamentals of object-oriented programming (OOP) using VB.NET. Chapter 1 provides a review of the syntax of VB.NET. This chapter is especially useful for readers who have experience with an older version of Visual Basic. Chapter 2 discusses the philosophy of OOP, including some sections on object-oriented design and abstract data types. Chapter 3 covers programming with structures, which are similar to user-defined types (UDTs) in Visual Basic 6.

Serialization is the process of capturing the current state of a class object and writing the state to disk. Serialization allows you to make a class object persistent, which means that you can save the current state of an object while a program is running and at a later time retrieve that state and continue using the object. In this chapter, we'll show you how to perform both serialization and deserialization, which is retrieving an object's state from disk.

SERIALIZATION DEFINED

Serialization in VB.NET involves writing out the state of a class object as a series of bytes to a byte stream. The CLR writes out a class object as an object-graph, which consists of the class object and all the member data associated with the object. To let the CLR know that a class can be serialized, it must be marked with the Serializable attribute.

Although classes must be marked to be serialized, primitive types do not have to be marked as such. Therefore, all the primitive types within your class definition will be serialized automatically when the class is marked Serializable. Other objects (such as nested classes) within a class definition must be tagged with the Serializable attribute if they are to be serialized with the rest of the class types.

A class is physically serialized using a formatter. A formatter, as its name suggests, defines the format of the data stream that is written to disk.