The paper presents two formal models for parallel computation: an abstract conceptual model and a parallel-program model. The conceptual model does not distinguish between control and data states, while the parallel-program model allows an infinite set of control states by representing multiple instruction pointers or processes executing the program. An induction principle is introduced to treat control and data state sets on the same ground, using "place variables" to express correctness conditions without enumerating all possible control states. The principle is demonstrated through examples of mutual exclusion proofs. The paper also discusses the limitations of assertions-oriented proof methods, introduces the concept of a "norm" for proving termination, and extends the program model to include local variables and shared global variables. The author argues that the induction principle is more powerful and succinct than the assertions method, which can be incomplete for certain cases. The paper concludes with extensions to handle more complex scenarios, including processes with their own local variables and an arbitrary number of dynamically created processes.The paper presents two formal models for parallel computation: an abstract conceptual model and a parallel-program model. The conceptual model does not distinguish between control and data states, while the parallel-program model allows an infinite set of control states by representing multiple instruction pointers or processes executing the program. An induction principle is introduced to treat control and data state sets on the same ground, using "place variables" to express correctness conditions without enumerating all possible control states. The principle is demonstrated through examples of mutual exclusion proofs. The paper also discusses the limitations of assertions-oriented proof methods, introduces the concept of a "norm" for proving termination, and extends the program model to include local variables and shared global variables. The author argues that the induction principle is more powerful and succinct than the assertions method, which can be incomplete for certain cases. The paper concludes with extensions to handle more complex scenarios, including processes with their own local variables and an arbitrary number of dynamically created processes.