Myers [My 90] makes compelling arguments that an introduction to formal methods should be a part of introductory computer science courses. Such methods include the topics of proof of program correctness, analytic methods of transformation and simplification of programs, etc. Since both Scheme and J are derived from formal mathematical notation it is not surprising that they may be used to introduce and describe formal methods in computer science. In [Ive 95], Iverson describes J as "... a formal imperative language. Because it is imperative, a sentence in J may also be called an instruction, and may be executed to produce a result. Because it is formal and unambiguous it can be executed mechanically by a computer, and is therefore called a programming language. Because it shares the analytic properties of mathematical notation, it is also called an analytic language."