C0 Libraries
15-122: Principles of Imperative Computation
Frank Pfenning
Sunday 23
rd
January, 2022
Compiler revision 707
(updates since September 2011)
Contents
1 Introduction 2
2 Input/Output 2
2.1 conio . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 2
2.2 file . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 3
2.3 args . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 4
3 Strings 5
3.1 parse . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 5
3.2 string . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 6
4 Images 8
4.1 img . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 8
5 C0-implemented libraries 9
5.1 rand . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 9
5.2 util . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 9
6 Updates 10
List of C0 Library Functions 12
SUNDAY 23
RD
JANUARY, 2022
Libraries C0.2
1 Introduction
This document describes the standard libraries available for use in the C0
language implementation. All libraries can be used with the cc0 compiler,
and most can also be used with coin. Please consult the C0 Tutorial and C0
Language Reference for more information on C0.
Libraries can be include on the command line using -l lib or in files
with #use <lib>. The latter is recommended to make source files less de-
pendent on context. Each library will be loaded at most once.
2 Input/Output
2.1 conio
The conio library contains functions for performing basic console input and
output. Note that output may be buffered, which means output does not
necessarily appear on the console until a newline character is printed or
flush() is called.
void print(string s); // print s to standard output
void println(string s); // print s with trailing newline
void printint(int i); // print i to standard output
void printbool(bool b); // print b to standard output
void printchar(char c); // print c to standard output
void flush(); // flush standard output
bool eof(); // test end-of-file on standard input
string readline() // read a line from standard input
/
*
@requires !eof(); @
*
/ ; // do not include the trailing newline
The printf function is also available when conio is imported. The ad-
dress of printf cannot be taken using & in C1.
/
*
Prints message and args to standard output.
*
’msg’ must be a string literal.
*
Available format specifiers:
*
%s: string argument
*
%d: int argument
*
%c: char argument
*
%%: literal % sign
*
The number and types of format specifiers must
*
match with the arguments provided
*
/
void printf(string msg, ...args);
SUNDAY 23
RD
JANUARY, 2022
Libraries C0.3
2.2 file
The file library contains functions for reading files, line by line. File han-
dles are represented with the file
_
t type. The handle contains an internal
position which ranges from 0 to the logical size of the file in byes. File han-
dles should be closed explicitly when they are no longer needed to release
system resources.
// typedef
______
*
file
_
t; /
*
file handle or NULL
*
/
/
*
Test whether the given file has been closed
*
/
bool file
_
closed(file
_
t f)
/
*
@requires f != NULL; @
*
/ ;
/
*
Create a handle for reading from the file given by the specified
*
path, NULL if the file cannot be opened for reading.
*
/
file
_
t file
_
read(string path)
/
*
@ensures \result == NULL || !file
_
closed(\result); @
*
/ ;
/
*
Release any resources associated with the file handle. This
*
function should not be invoked twice on the same handle.
*
/
void file
_
close(file
_
t f)
/
*
@requires f != NULL; @
*
/
/
*
@requires !file
_
closed(f); @
*
/
/
*
@ensures file
_
closed(f); @
*
/ ;
/
*
Test if we have read the whole file.
*
/
bool file
_
eof(file
_
t f)
/
*
@requires f != NULL; @
*
/
/
*
@requires !file
_
closed(f); @
*
/ ;
/
*
Read a line from the given file (without the trailing newline)
*
and advance the handle’s internal position by one line. The
*
contract requires that the handle is not at the end-of-file,
*
so this must be checked before (with file
_
eof).
*
/
string file
_
readline(file
_
t f)
/
*
@requires f != NULL; @
*
/
/
*
@requires !file
_
closed(f); @
*
/
/
*
@requires !file
_
eof(f); @
*
/ ;
SUNDAY 23
RD
JANUARY, 2022
Libraries C0.4
2.3 args
The args library provides function for basic parsing of command line argu-
ments provided to the executable provided by the cc0 compiler. The args
library is not supported by coin since it never produces an executable.
/
*
Add a flag with the given name. During parsing if that flag is
*
set (with -name on the command line), it writes the value true
*
to the location given by ptr.
*
/
void args
_
flag(string name, bool
*
ptr)
/
*
@requires ptr != NULL; @
*
/ ;
/
*
Add an integer option with the given name. During parsing if
*
that option is given (with -name <int>) it attempts to parse
*
it as an integer and write it to the location given by ptr.
*
/
void args
_
int(string name, int
*
ptr)
/
*
@requires ptr != NULL; @
*
/ ;
/
*
Add an string option with the given name. During parsing if
*
that option is given (with -name <string>) it write it to the
*
location given by ptr.
*
/
void args
_
string(string name, string
*
ptr)
/
*
@requires ptr != NULL; @
*
/ ;
struct args {
int argc;
string[] argv;
};
typedef struct args
*
args
_
t;
/
*
Parse the program’s arguments according to any flags and options
*
set up by previous calls. Any unrecognized arguments are returned
*
in order in \result->argv.
*
*
If there is an error, args
_
parse will return NULL.
*
/
args
_
t args
_
parse()
/
*
@ensures \result == NULL
|| \result->argc == \length(\result->argv); @
*
/ ;
SUNDAY 23
RD
JANUARY, 2022
Libraries C0.5
3 Strings
3.1 parse
The parse library provides functions to convert strings to booleans or inte-
gers and for whitespace-tokenizing a string. This is useful, for example, if
you want to convert strings read from a file into integers. The parse
_
ints
function is aimed more at unit tests than user input.
/
*
Attempt to parse "true" or "false from s and return a pointer to
*
the result or NULL if not of that form.
*
/
bool
*
parse
_
bool(string s);
/
*
Attempt to parse an integer from the given string.
*
For base > 10, the letters A-Z (case insignificant) are used as
*
digits. Return NULL if s cannot be completely parsed to an int
*
in the given base.
*
/
int
*
parse
_
int(string s, int base)
/
*
@requires 2 <= base && base <= 36; @
*
/ ;
/
*
Returns the number of whitespace-delimited tokens in a string
*
/
int num
_
tokens(string s);
/
*
Returns true iff the string contains only whitespace separated
*
ints
*
/
bool int
_
tokens(string s, int base)
/
*
@requires 2 <= base && base <= 36; @
*
/ ;
/
*
Parses a string as a list of whitespace-delimited tokens
*
/
string[] parse
_
tokens(string s)
/
*
@ensures \length(\result) == num
_
tokens(s); @
*
/ ;
/
*
Parses a string as list of whitespace-delimited integers
*
/
int[] parse
_
ints(string s, int base)
/
*
@requires int
_
tokens(s, base); @
*
/
/
*
@ensures \length(\result) == num
_
tokens(s); @
*
/ ;
SUNDAY 23
RD
JANUARY, 2022
Libraries C0.6
3.2 string
The string library contains a few basic functions for working with strings
consisting of ASCII characters. For most nontrivial tasks, it is best to con-
vert back and forth between characters arrays and strings, using the func-
tions string
_
to
_
chararray and string
_
from
_
chararray. The two are iden-
tified in C, but distinguished in C0 to allow a type-safe and memory-safe
implementation. Note that character arrays should contain a trailing ’\0’
character not present in the corresponding strings.
/
*
Return length of s, in characters.
*
May be an O(n) operation.
*
/
int string
_
length(string s);
/
*
Return s[idx] and abort if the idx is out of bound.
*
May be an O(n) operation.
*
/
char string
_
charat(string s, int idx)
/
*
@requires 0 <= idx && idx < string
_
length(s); @
*
/ ;
/
*
Return a new string that is the result of concatenating a
*
and b.
*
/
string string
_
join(string a, string b)
/
*
@ensures string
_
length(\result)
== string
_
length(a) + string
_
length(b); @
*
/ ;
/
*
Returns the substring composed of the characters of s beginning
*
at the index given by start and continuing up to but not
*
including the index given by end. If end == start, the empty
*
string is returned. Aborts if start or end are out of bounds,
*
or end < start.
*
/
string string
_
sub(string a, int start, int end)
/
*
@requires 0 <= start && start <= end && end <= string
_
length(a); @
*
/
/
*
@ensures string
_
length(\result) == end - start; @
*
/ ;
/
*
Compare strings lexicographically
*
/
bool string
_
equal(string a, string b);
/
*
string
_
compare(a, b) returns
*
\result < 0 if a comes lexicographically before b
*
\result == 0 if a and b are the same string
*
\result > 0 if a comes lexicographically after b
*
/
int string
_
compare(string a, string b);
/
*
Create strings from other basic values
*
/
string string
_
fromint(int i);
string string
_
frombool(bool b);
SUNDAY 23
RD
JANUARY, 2022
Libraries C0.7
string string
_
fromchar(char c)
/
*
@requires c != ’\0’; @
*
/
/
*
@ensures string
_
length(\result) == 1; @
*
/
/
*
@ensures string
_
charat(\result, 0) == c; @
*
/ ;
/
*
Convert every uppercase character A-Z to lowercase a-z
*
/
string string
_
tolower(string s);
/
*
Check if character array is properly \0-terminated
*
/
bool string
_
terminated(char[] A, int n)
/
*
@requires 0 <= n && n <= \length(A); @
*
/ ;
/
*
Construct a ’\0’-terminated character array from s
*
/
char[] string
_
to
_
chararray(string s)
/
*
@ensures \length(\result) >= string
_
length(s) + 1; @
*
/
/
*
@ensures string
_
terminated(\result, string
_
length(s) + 1); @
*
/ ;
/
*
Construct a string from the the array A up to (but not
*
including) the terminating ’\0’
*
/
string string
_
from
_
chararray(char[] A)
/
*
@requires string
_
terminated(A, \length(A)); @
*
/
/
*
@ensures string
_
length(\result) + 1 <= \length(A); @
*
/ ;
/
*
Convert between characters and their ASCII value
*
/
int char
_
ord(char c)
/
*
@ensures 0 <= \result && \result <= 127; @
*
/ ;
char char
_
chr(int n)
/
*
@requires 0 <= n && n <= 127; @
*
/ ;
Similiar to conio, the format function is available when importing string.
The address of format cannot be taken using & in C1.
/
*
Acts like ’printf’, but returns the result as a
*
string instead of printing it.
*
’msg’ must be a string literal.
*
Available format specifiers:
*
%s: string argument
*
%d: int argument
*
%c: char argument
*
%%: literal % sign
*
The number and types of format specifiers must
*
match with the arguments provided
*
/
string format(string msg, ...args);
SUNDAY 23
RD
JANUARY, 2022
Libraries C0.8
4 Images
4.1 img
The img library defines a type for two-dimensional images represented with
4-channel color—alpha, red, green and blue— packed into one int It de-
fines and image type image
_
t. Like file handles, images must be explicitly
destroyed when they are no longer needed; the garbage collector will not
be able to free them.
// typedef
______
*
image
_
t; /
*
image handle or NULL
*
/
/
*
Retrieves the width of the given image
*
/
int image
_
width(image
_
t image)
/
*
@requires image != NULL; @
*
/
/
*
@ensures \result > 0; @
*
/ ;
/
*
Retrieves the height of the given image
*
/
int image
_
height(image
_
t image)
/
*
@requires image != NULL; @
*
/
/
*
@ensures \result > 0; @
*
/ ;
/
*
Creates an ARGB image with dimensions width
*
height
*
/
image
_
t image
_
create(int width, int height)
/
*
@requires 0 < width && 0 < height; @
*
/
/
*
@ensures \result != NULL; @
*
/
/
*
@ensures image
_
width(\result) == width; @
*
/
/
*
@ensures image
_
height(\result) == height; @
*
/ ;
/
*
Copies an existing image
*
/
image
_
t image
_
clone(image
_
t image)
/
*
@requires image != NULL; @
*
/
/
*
@ensures image
_
width(\result) == image
_
width(image); @
*
/
/
*
@ensures image
_
height(\result) == image
_
height(image); @
*
/ ;
/
*
Returns a copy of a subrectangle of the given image. The new
*
image has dimensions width
*
height. If part of the given
*
rectangle is not contained within the given image, those pixels
*
are assumed to be transparent black.
*
/
image
_
t image
_
subimage(image
_
t image, int x, int y, int width, int height)
/
*
@requires image != NULL; @
*
/
/
*
@ensures image
_
width(\result) == width; @
*
/
/
*
@ensures image
_
height(\result) == height; @
*
/ ;
/
*
Loads an image from the given path and convert it if need be
SUNDAY 23
RD
JANUARY, 2022
Libraries C0.9
*
to an ARGB image. If the file does not exist, it returns NULL.
*
Aborts if the file has the wrong format.
*
/
image
_
t image
_
load(string path);
/
*
Saves the given image to disk, inferring the file type from the
*
file extension given in the path.
*
/
void image
_
save(image
_
t image, string path)
/
*
@requires image != NULL; @
*
/ ;
/
*
Returns an array of pixels representing the image. The pixels
*
are given line by line so a pixel at (x,y) would be located at
*
y
*
image
_
width(image) + x. Any writes to the array will be
*
reflected in calls to image
_
save, image
_
clone and image
_
subimage.
*
The channels are encoded as 0xAARRGGBB.
*
/
int[] image
_
data(image
_
t image)
/
*
@requires image != NULL; @
*
/
/
*
@ensures \length(\result)
== image
_
width(image)
*
image
_
height(image); @
*
/ ;
5 C0-implemented libraries
A few libraries are included as part of the default C0 distribution but are
implemented in C0, not in C. Both the interface (.h0) and the implementa-
tion (.c0) of these libraries are provided in the lib directory.
5.1 rand
// typedef
_____
*
rand
_
t;
rand
_
t init
_
rand (int seed)
/
*
@requires seed != 0; @
*
/
/
*
@ensures \result != NULL @
*
/ ;
int rand(rand
_
t gen)
/
*
@requires gen != NULL; @
*
/ ;
5.2 util
/
*
C0 constants
*
/
int int
_
size() /
*
@ensures \result == 4; @
*
/ ;
int int
_
max() /
*
@ensures \result == 2147483647; @
*
/ ;
int int
_
min() /
*
@ensures \result == -2147483648; @
*
/ ;
/
*
Absolute value
*
/
SUNDAY 23
RD
JANUARY, 2022
Libraries C0.10
int abs(int x)
/
*
@requires x > int
_
min(); @
*
/
/
*
@ensures \result >= 0; @
*
/
/
*
@ensures \result == (x < 0 ? -x : x); @
*
/ ;
/
*
Maximum of two integers
*
/
int max(int x, int y)
/
*
@ensures \result == x || \result == y; @
*
/
/
*
@ensures \result >= x && \result >= y; @
*
/ ;
/
*
Minimum of two integers
*
/
int min(int x, int y)
/
*
@ensures \result == x || \result == y; @
*
/
/
*
@ensures \result <= x && \result <= y; @
*
/ ;
/
*
Returns the hexidecimal representation of the given integer
*
as a string (without the leading 0x)
*
/
string int2hex(int x);
6 Updates
Rev. C0.0011, Jan 06, 2012. Image Library. image
_
destroy has been depre-
cated, since images are now garbage collected. Contracts on image
functions have been sharpened to require strictly positive height and
width. image
_
load returns NULL if the file does not exist or is not read-
able.
Rev. C0.0113, Sep 27, 2012. Conio Library. Function eof has been added
to test end-of-file along standard input. This fixes a problem with ^D
during readline and end of stream for shell redirect to stdin. readline
now requires !eof().
Rev. C0.0167, Dec 8, 2012. Conio Library. Function error has been removed
from the conio library, since it now exists as a language primitive.
Rev. C0.0273, Feb 1, 2013. Add util and rand libraries.
Rev. C0.0438, January 8, 2015. Remove deprecated image
_
destroy function,
add max and min to util and add num
_
tokens, parse
_
tokens, int
_
tokens,
and parse
_
ints to the parse library. Formatting changes.
Rev. C0.0590, March 30, 2018. Reformatted documentation to use the listings
Latex package.
SUNDAY 23
RD
JANUARY, 2022
Libraries C0.11
Rev. C0.0590, December 20, 2019. Added the table of contents and index.
Rev. C0.0707, August 18, 2020. Added printf and format.
SUNDAY 23
RD
JANUARY, 2022
List of C0 Library Functions
abs, 10
args
_
flag, 4
args
_
int, 4
args
_
parse, 4
args
_
string, 4
args
_
t, 4
char
_
chr, 7
char
_
ord, 7
eof, 2
file
_
close, 3
file
_
closed, 3
file
_
eof, 3
file
_
read, 3
file
_
readline, 3
file
_
t, 3
flush, 2
format, 7
image
_
clone, 8
image
_
create, 8
image
_
data, 9
image
_
height, 8
image
_
load, 9
image
_
save, 9
image
_
subimage, 8
image
_
t, 8
image
_
width, 8
init
_
rand, 9
int2hex, 10
int
_
max, 9
int
_
min, 9
int
_
size, 9
int
_
tokens, 5
max, 10
min, 10
num
_
tokens, 5
parse
_
bool, 5
parse
_
int, 5
parse
_
ints, 5
parse
_
tokens, 5
print, 2
printbool, 2
printchar, 2
printf, 2
printint, 2
println, 2
rand, 9
rand
_
t, 9
readline, 2
string
_
charat, 6
string
_
compare, 6
string
_
equal, 6
string
_
from
_
chararray, 7
string
_
frombool, 6
string
_
fromchar, 7
string
_
fromint, 6
string
_
join, 6
string
_
length, 6
string
_
sub, 6
string
_
terminated, 7
string
_
to
_
chararray, 7
string
_
tolower, 7
SUNDAY 23
RD
JANUARY, 2022
