Semantics for a Distributed Programming Language Using SACS and Weakest Pre-Conditions

This paper describes the semantics for a distributed programming language called LIPS (language for implementing parallel systems). The formalism presented is used for the specification and verification of LIPS programs for the successful point-to-point intercommunication in distributed systems. The main focus of the paper is to define the semantics of the computational part of LIPS using Dijkstra´s weakest preconditions and demonstrate the integration of SACS(specification of asynchronous communication systems) with GCL(guarded command language) using an example. SACS is a variant of SCCS specially developed for specifying point-to-point asynchronous message passing systems.