This paper describes a method to determine the possibility of combining two or more process models using an approach similar to the proof of (partial) correct- ness of algorithms by determining the weakest precon- dition and postcondition. This method also allows the analysis of process models with regard to their semantic correctness. The approach is described and demonstrated on an example process.