1package Synchronized1
2  with SPARK_Mode,
3       Abstract_State => (State with Synchronous),
4       Initializes    => State
5is
6   procedure Force_Body;
7end Synchronized1;
8