Deriving a dynamic programming algorithm for batch scheduling in the refinement calculus

---

Thesis Type: Postgraduate

Institution Of The Thesis: Middle East Technical University, Faculty of Engineering, Department of Computer Engineering, Turkey

Approval Date: 2003

Thesis Language: English

Student: İrem Aktuğ

Supervisor: MEHMET HALİT S. OĞUZTÜZÜN

Abstract:

Refinement Calculus is a formalization of stepwise program construction.In this approach a program is derived from its specification by applying refinement rules.The Refinement Calculator,developed at TUCS,Finland,provides tool support for the Refinement Calculus.This thesis presents a case study aiming to evaluate the applicability of the theory and the performance of the tool.The Refinement Calculator is used for deriving a dynamic progaramming algorithm for a single-machine batch scheduling problem.A quadratic algoritm is derived by refining a formal specification of this problem into executable code.The need for stronger support for relevant domain theories and abstraction mechanisms in the target language have been noted.