There is a resurgence of interest on online Machine Translation (MT) after web becomes a prime vehicle for disseminating information in multilingual cyberspace. Compared to traditional MT, OnlineMT is a research focusing on both Multilingual Computing and Computational Simulation. In order to supply a justification for Multilingual Computing, computing-free theorems are broached and proven using formal methods in this thesis. Because distributed computing technique is used in most of Multilingual Computing systems, a mechanized Hoare logic is proposed and implemented by us to prove the security of distributed computing. Basing on computing-free theorems, we implement an online domain-based Portuguese-Chinese machine translation system (onlineDBMT). From the point of Computational Simulation, onlineDBMT provides an insight into how translation is performed, In the last, a framework for multilingual computing is proposed. Keywords: multilingual, domain-specific, computing-free, distributed computable