Using Coq in specification and program extraction of hadoop mapreduce applications

摘要: Hadoop MapReduce is a framework for distributed computation on key-value pairs. The goal of this research to verify actual running code applications. We first constructed an abstract model with the proof assistant Coq. In model, mappers and reducers in are modeled as functions Coq, specification application expressed terms invariants among involving its mapper reducer. also provides modular proofs lemmas that do not depend To achieve goal, we investigated feasibility two approaches. one approach, transformed verified reducer into Haskell programs executed them under Streaming. other JML annotations Java using Krakatoa, translated Coq axioms, proved specifications from them. either were able correctness applications actually run framework.