The Use of Typed Lambda Calculus for Requirements Capture in the Domain of Ecological Modelling

We will describe the use of order-sorted, typed lambda calculus to represent ecological simulation models. It will be used to represent both the qualitative specifications of ecological situations and the differential equations which describe these situations quantitatively. The numerical solution of these equations constitutes a simulation model of the situation. This logic-based formalism extends previous formalisms for ecological modelling. Particular emphasis will be given to the automatic help given to users in formulating their goals, describing the ecological situation to be modelled and forming the differential equations which model it. The typed lambda calculus representation provides a simple grammar for constraining and guiding this process of requirements capture. Users develop their goals by a process of refinement of logical expressions. Each refinement step can also be understood in ecological terms. The refinement steps are necessarily not truth preserving because we are engaged in requirements capture rather than specification
transformation.