Data mining, which is a technology for obtaining useful knowledge from large database, has been gradually recognized as an important subject. Algorithms for data mining have to be efficient since target database is often huge, and various kinds of efficient algorithms for data mining are individually investigated. This paper shows that an efficient linear time algorithm for mining optimized gain association rules can be systematically derived from a simple specification by reducing it to an instance of the maximum marking problem. Our approach not only automatically guarantees the correctness of the derived algorithm, but also is easy to derive new algorithms for modification of the problem.