To expand the horizons, means and methods of formal studying on service computing, a formal service computing model for Web service is built. Since a great number of service entities are from different third-party providers in open network, software entities are abstracted as coalgebraic monads, then a semantic model is given for services in the black-box method. Based on coalgebraic monads, a formal framework is put forward for service-oriented computing (SOC) with its applications as well. Finally, a prototype system is implemented for service computing based on monads, which supports service abstraction, publishing, discovery and metrics from legacy systems.