Communications of the ACM

Training sessions are good opportunities to present students with challenging programming problems that cannot be solved without theoretical background in spite of simple formulation. The trainers should provide students with background theory as soon as students realize the programming complexity of these problems.

A natural question arises: how to engage undergraduates with theory through programming contests? The first possibility, of course, is during training sessions. Training sessions are good opportunities to present students with challenging programming problems that cannot be solved without theoretical background in spite of simple formulation. The trainers should provide students with background theory as soon as students realize the programming complexity of these problems. We would like to sketch here a brief example of how a program logic's tributary creek of a powerful stream called formal methods can be presented in a popular (but mathematically sound) form to undergraduate students of computer science, mathematics, physics, and technical departments.

Before presenting our experiences we discuss the second opportunity for increasing the influence of ACM programming contests on better computer science education. We believe organizers of regional- and international-level contests should provide (after competition) comprehensive Web-based tutorials on how to solve selected problems with background theory and sample programs. The importance of these tutorials is key.

• a number N of coins under question;
• a number M of marked valid coins; and
• a limit K of balancings

which outputs either "impossible" or another executable interactive program ALPHA (in the same language) with respect to the existence of a strategy to identify a unique false coin among N coins with use of M marked valid coins and balancing K times at most. ALPHA should implement an identification strategy in the following settings. Each session with ALPHA begins from user choice of the false coin's number and whether it is lighter or heavier. Then a session consists of a series of rounds and the number of rounds in the session cannot exceed K. On each round the program outputs two disjoint subsets of numbers of coins to be placed on pans of a balance. User in his/her turn replies in accordance with his/her initial choice. The session should finish with the final output of the program ALPHA—the false coin's number.

Since the problem is to write a program that produces another program, we refer to the problem as the metaprogram problem.

In this metaprogram problem case the following game interpretation (which is very popular in mathematics and computer science theory) is useful due to its methodological and pedagogical importance. Let M and N be non-negative integer parameters and let (N+M) coins be enumerated by consequent numbers from 1 to (N+M). Coins with numbers in [1...M] are valid while there is a unique false coin among those with numbers in [(M+1)...(M+N)]. A GAME(N,M) of two players User and Prog consists of a series of rounds. On each round a move of Prog is to partition the coins for the balancing: a pair of disjoint subsets (with equal cardinalities) of [1...(M+N)]. A possible move of User is either <, = or >, but his/her reply must be consistent with all constraints induced in previous rounds. Prog wins GAME(N,M) as soon as a unique number in [1...(M+N)] satisfies all constraints induced during the game. In this setting the metaprogram problem can be reformulated as follows:

Write a program which, for all N ^ 1, K ^ 0, and M ^ 0, generates (if possible) a winning strategy in GAME(N,M) for Prog that uses at most K rounds.

What is a proper formalism for solving the metaprogram problem in this new setting? A hint is that a formalism should have explicit fixed-points. The following informal statement is very natural for every finite game of two players A and B: that a player A is in a position where he/she wins against B is equivalent to that A has a move prior to and after which the game is not lost, but after which every move of B leads to a position where (again) A wins against B. In other words: a set of positions with a winning strategy is a fixed-point of some transformation of sets of positions.

A functional paradigm is a well-known paradigm with explicit fixed-points, and the metaprogram problem can be solved in this framework. But, in accordance with regulations of ACM Collegiate Programming Contests, programs should be written in an imperative language such as Pascal, C, C++, or Java. So another paradigm would be better in this case than the functional one. It should be a paradigm that captures imperative style and fixed-points simultaneously. This is a Program Logics paradigm in general, and the formalism of the propositional mu-Calculus [3] in particular. But this formalism is in the most comprehensive form that relies upon transfinite induction and some basic modal logics: it is not easy to make the mu-Calculus easy for undergraduates. In this case another hint is an incremental approach to the introduction of the mu-Calculus in finite models only. The technical details of this approach are not appropriate for a Communications article, but readers should be aware the technical memo Program Logics Made Easy, which contains a solution for the metaprogram problem and background theory, is available on the Web [4].

• Programming contests are a good opportunity for better education and popularization of computer science theory and mathematical foundations of formal methods;
• Computer science journals and magazines should promote popularization of computer science theory; and
• An attitude of theorists to the popularization and contests should and can be improved.