Formal Modeling in RISCAL
RISCAL (RISC Algorithm Language) is a language and associated software system for formalizing mathematical models and algorithms and automatically checking the formalization over finite domains. Your task is to study a particular mathematical/computational problem from literature, to develop a formal model of this problem in the RISCAL language, and to validate this model with the RISCAL software. The model may be the specification of a computational problem by a pair of pre/post-conditions; these may be validated by analyzing the inputs/output pairs allowed by the specification and by checking the correctness of an algorithm with respect to this specification. The model may also describe a computational system by an initial state condition and a transition relation; these may be validated by analyzing the sequences of system states arising from this model.