In this chapter, we shall see how to develop sequential programs. We present the approach we shall use, and then we propose a large number of examples.

Sequential programs (e.g. loops), when formally constructed, are usually developed gradually by means of a series of progressively more refined “sketches” starting with the formal specification and ending in the final program. Each such sketch is already (although often in a highly non-deterministic form) a monolithic description which resumes the final intended program in terms of a single formula. This is precisely that initial “formula”, that is gradually transformed into the final program.

We are not going to use this approach here. After all, in order to prove a large formula, a logician usually breaks it down into various pieces, on which he performs some simple manipulations before putting them together again in a final proof.

A systematic approach to sequential program development

Components of a sequential program

A sequential program is essentially made up of a number of individual assignments that are glued together by means of various constructs. Typical constructs are sequential composition (;), loop (while), and condition (if). Their role is to explicitly schedule these assignments in a proper order so that the execution of the program can achieve its intended goal.

This final chapter is entirely devoted to problems which you might try solving. They are all to be done with the Rodin Platform, which you can download from the web site “event-b.org”. We recommend beginners who are downloading the Rodin Platform for the first time to “perform” the tutorial which is included on this site before engaging in any of the problems presented in this chapter.

These problems are divided up into three categories called Exercises (Section 1), Projects (Section 2), and Mathematical developments (Section 3).

Exercises are small and easy developments, mainly corresponding to the construction of simple sequential programs. But we also find models of simple complete systems and even the development of a small electronic circuit. Exercises can be proposed in a beginner course.

Projects are more serious problems, which require more investment than exercises. They can be proposed in an advanced course.

Mathematical developments come from pure mathematics. They involve more complicated proofs than in the two previous cases; most of them are not performed automatically by the provers of the Rodin Platform. As such, they represent excellent exercises to improve our ability to perform interactive proofs.

For Exercises and Projects, we are required to write a requirements document as well as a refinement strategy before engaging in the formal development with the Rodin Platform. Most of the time, we will have to use some contexts to define the carrier sets and the constants of the problem at hand.

This title is certainly provocative. We all know that this claim corresponds to something that is impossible. No! We cannot construct faultless systems; just have a look around. If it were possible, it would have been already done a long time ago. And anyway, to begin with, what is a “fault”?

So, how can we imagine the contrary? We might think: yet another guru trying to sell us his latest universal panacea. Dear reader, be reassured, this Prologue does not contain any new bright solutions and, moreover, it is not technical; you'll have no complicated concepts to swallow. The intention is just to remind you of a few simple facts and ideas that you might use if you wish to do so.

The idea is to play the role of someone who is faced with a terrible situation (yes, the situation of computerized system development is not far from being terrible – as a measure, just consider the money thrown out of the window when systems fail). Faced with a terrible situation, we might decide to change things in a brutal way; it never works. Another approach is to gradually introduce some simple features that together will eventually result in a global improvement of the situation. The latter is the philosophy we will use here.

Introduction

The intent of this chapter is to introduce a complete example of a small system development. During this development, we will become aware of the systematic approach we are using: it consists in developing a series of more and more accurate models of the system we want to construct. This technique is called refinement. The reason for building consecutive models is that a unique one would be far too complicated to reason about. Note that each model does not represent the programming of our system using a high-level programming language, it rather formalizes what an external observer of this system could perceive of it.

Each model will be analyzed and proved, thus enabling us to establish that it is correct relative to a number of criteria. As a result, when the last model is finished, we will be able to say that this model is correct by construction. Moreover, this model will be so close to a final implementation that it will be very easy to transform it into a genuine program.

The correctness criteria alluded to above will be made completely clear and systematic by giving a number of proof obligation rules which will be applied on our models. After applying such rules, we shall have to prove formally a number of statements. To this end, we shall also give a reminder of the classical rules of inference of the sequent calculus. Such rules concern propositional logic, equality, and basic arithmetic.

VB Quip

The world runs on databases. The modern world relies on them and would be lost without them. Business depends on them, from storing employee and payroll data, to customer data, supplies, manufacturing, transportation, and inventory – you name it. It seems like everything these days is on the computer. In fact, if it's not on the computer, it's probably old and outdated. The key then, is being able to access these data, manipulate them, update them, search them, sort them, and make them work for you. That's where LINQ to SQL comes in. It's the connection between your VB program and a database. In this case, it's an Access file, but the same principles hold true for access to almost any type of database. You'll get the basics to connect to a database, view it, update it, and use it. It takes several programming classes and a couple of database classes to get good at it, but here you'll get a taste of it and some general principles to get you started.

Background

Databases come in several forms, but by far the most popular database management system (DBMS) is a relational database.

VB Quip

By now you've come to realize that the real bottlenecks of your programs are input and output. Some of that is because users can only type and click so much and some of it is because input is repetitive. You've created useful output but have been unable to hang on to it. So far, every program run has meant starting from scratch with your data, entering it as needed, calculating the results, and then losing all of that work with a click of the Exit Button. No more. File input and output gives you the ability to store data and retrieve it as needed. File input takes data stored in a file and puts it into your program. File output stores the results in a file so you can use the data at a later date. This chapter covers the details of opening a data file, reading the data, processing the data, displaying the output, and writing the results to a file.

The Basics of File Input and Output

A data file, for our purposes, is a text file. Each line in the file is a record. A record consists for one or more fields.

VB Quip

Think of objects as tools. Better yet, think of them as building blocks. Imagine how hard a job would be if you had to create everything from scratch every time. Say you wanted to build a table. First, you'd need to make an axe to cut down the tree. Then you'd have to make a saw to cut the wood. You'd have to make your own nails to piece together the table, but that's only after you made your own hammer so you could pound the nails. Programming is like that sometimes – OK, usually. And it was certainly that way years ago. Everything was done from scratch and very little was reusable. However, there's been some progress since then. You saw reusable code when you learned procedures and functions. Objects and classes are that way, but on a grander scale. The controls in the Toolbox are objects, each specially created for a specific task. They're tools and, without them, development would be much tougher, and a whole lot less fun. Classes are code that defines an abstract data type – it's a thing, and the developer provides a description of it and determines how it can be used. This chapter shows you how to create objects with your code and how to define and use classes.

VB Quip

We live in a world of specialization. Want a cup of coffee? There's a store that specializes in coffee, any way you like it. Need a doughnut to go with it? There's a company that makes and sells the best doughnuts. Need something to read while you're enjoying a bite? Pick from thousands of magazines or millions of books on any and all topics imaginable. Gone are the days of the local handyman – the resident “Mr. Fixit” – who could fix anything and get anything to work. Today's world has specialists. A mechanic specializes in car repair. The cable guy handles your TV problems. When the office copier is on the fritz, call the copier guy. Everyone's an expert.

Programming is the same way. Blocks of code are written for a particular purpose. Some do simple tasks, but do them often. It's easier to write a procedure once for a task and then call it multiple times as needed. Other blocks of code might do a complicated calculation or solve a particular problem. These provide a specific function. It's easier to write and store these functions and then use them when needed than it is to create them from scratch. That's the basis for procedures and functions.

VB Quip

On a computer, memory is everything, or nearly so. Data are stored there and programs are loaded and run from memory. Memory is essential. Compared to what was available a few years ago, today's computers have a huge amount of memory. A few years ago that same comparison would have been true as well. Forty years ago we sent men to the moon with spaceships that had less memory than a good pocket calculator has today. All computers, old and new, have memory in common. Memory is where what the computer “knows” is stored. Much of programming comes down to allocating and managing memory. For the PCs of a generation ago, memory was a scarce and expensive commodity to be guarded closely and used judiciously. Programmers used it carefully and squeezed as much as they could from it. At the time, conserving memory gave you a leg up on development and helped make your programs faster and more efficient. And, today, while the amount of memory isn't as much of an issue, the management of memory is. When you work on your computer, you work with its “desktop.” These days, it's the size of a table. In the early days of programming, that “desktop” was the size of a postage stamp. Variables and constants are two important components of a computer program. Both are created in memory and are assigned values.

VB Quip

“A picture is worth a thousand words,” or so said Frederick R. Barnard nearly ninety years ago. He was selling advertising for streetcars and couldn't have had computer graphics in mind. In fact, the first computer was still a generation away. But, he was pretty accurate because it just might take a thousand words of computer code to generate a good picture. Remember that the computer takes baby steps and every step has to be clearly described. The same is true with graphics. You can place pictures on your form and you can create graphics – beautiful graphics if you take the time – but you have to write some code to do it. Visual Basic can draw lines and shapes, it can work with text, and it's great with colors. It just takes a little work to create them and a little code to do it right. This chapter introduces the basics for graphics, sound, and multimedia. When it's over, you'll be able to play sound and video, create simple shapes, and draw and paint with the computer.

Graphic Basics

There are several ways to add graphics to a program. You've already worked with the PictureBox to add graphics. But there's so much more.

VB Quip

Good software does just that. It's easy to use, “intuitive” is the buzzword used in the industry. It does what it should and people actually like using it. Developers must keep two things in mind: getting the program to do what it should and making it useable – the two go hand-in-hand. A cool interface means nothing if the software doesn't perform. And, no matter how solid the code is, a clunky program is nearly worthless. Always think of both form and function. On the one hand, a developer must write code that works. On the other, a developer must always consider the end user. Never forget, you can't have one without the other!

New Events

You're familiar with several events such as Click, Load, and Scroll, but there are more, many more. In fact, there are far too many to cover in anything short of the dreaded user's manual. Every event can trigger code and every user action raises an event, that is, every time the user does something, from a click of the mouse to a peck of a key, a program can respond. How it responds and what it does are key to good software.

KeyPress

When a key is pressed, it generates a KeyPress event and also several other key events.

VB Quip

So far you have seen how a sequence of steps lets you build a program that will do your bidding. You've seen how decision structures give the computer the ability to make decisions. You've learned how to get the computer to repeat instructions, giving it the ability to do the same task over and over. And, you've taught it how to read and write. Well, it can't read and write, but it can access and store data in a file. All of these give the computer the ability to access and process data at remarkable speed. But, you've been limited to only a handful of names and numbers – only what you could hold in your hand and keep track of in your head. You've been forced to discard one thing in order to grab the next. It's as if the world was a full-screen movie and you're stuck looking at stills in the family photo album. Enter arrays. With an array you can grab an armful of data and process it as you wish. Instead of stills on Grandma's porch, you've got a DVD on HD and control of the remote.

VB Quip

The more work you put into your programs, the less work they'll be for the user. A developer might not like that, but a good program might be used hundreds or thousands of times by millions of users. If you make it just a little easier for every one of them every time they use it – well, you get the idea. Your programs aren't quite there yet, but the basic principles are the same. Just develop an interface with the user in mind and spend a little more time getting the details right. The interface takes care of input and output and the developer worries about the details to handle the processing that comes in between. Good programs are fun and easy to use. They allow the user to concentrate on solving a problem rather than forcing them to figure out how to use the computer.

This chapter introduces new tools. Most of them make it easier for the user and more complicated for the developer. There are also a few other odds and ends to clean up your output.

RadioButtons

RadioButtons are used to select one option from a list of several options. Click on a RadioButton to select it. A black dot appears inside the circle to indicate it's selected. Click on another RadioButton to select it and deselect the original.

VB Quip

That's a rather cavalier approach for anyone to take, especially when computers are involved. Knowledge is power and the more you know, the greater your power. One book isn't enough to give you all-consuming power, especially over a tool as powerful as a computer. It is, however, enough to get you started. One book won't turn you into a nerd that looks at his own shoes when talking, lives on caffeine and stale snack cakes, and would rather hack on a computer than go out on a date. That's just a stereotype perpetuated by teen movies. While it does fit a few people, almost all of the ones I know are smart, articulate, funny, and just all-around bright and inquisitive people. Above all, they're curious. And the best are curious about nearly everything, not just computers. How does it work? What happens when I try this? What if…?

Programming is, above all else, about thinking and problem-solving. If for no other reason, it's useful because it makes you think about thinking and makes you describe how to solve a problem. For the computer to solve a problem, even simple tasks must be explained in great detail. For someone to explain the rules to a computer – in other words, to write a program – takes a great deal of thinking and understanding.