Type Systems for Resource Use in Component Software

In many situations a programmer must be concerned with resources which are not accounted and controlled completely by the programming language. These could be external physical resources, like a printer or a screen, it could be more abstract physical resources, like computing time, memory usage, or writing some file to disk or it could be other software components or programs. The resources can be used directly by the program, or indirectly, through the use of libraries or other software. An important property of these resources is their externally, often physically, enforced limits, which are independent of program execution. Finding maximum and minimum number of active or used instances of these resources at some point during execution can be difficult and demand time from both programmer and computer. But this can also be important for safe execution. As a silly example, a program which every minute allocates, but fails to deallocate, 1 byte of memory, will at some point fail, while runtime testing might not reveal this before it is run for a week. Many of the new mobile and low-cost devices (e.g. the hundred dollar laptop http://laptop.org ) would probably also benefit from provable upper limits on the usage of some resources, like writing to the disk or memory. Developing static systems for finding some of these limits, is the goal in which this thesis hopes to take part. With “static” I mean systems which analyse the source code, not the execution of the compiled program