Circumcenter of a triangle

Circumcenter of a triangle

This an example from most elementary courses in geometry, i.e. in Euclidean geometry.

Specification

Text: construct the circumcenter of a triangle Specification: given: point A, point B, point C precondition: not collinear A B C find: O postcondition: |OA| = |OB| = |OC|

Program in GCL

1  Program circumcenter A B C O =
2    let (P_1, P_2) = Take \epsilon (Q_1, Q_2). Q_1 \in {A,B,C} \land
3     	       	      	   	    	  	Q_2 \in {A,B,C} \land not Q_1 = Q_2
4	 m_1 = Subproblem (Triangles, [geom, euclid, plane, median],
5	       		  	      [geom, euclid, plane, 2circ]) P_1 P_2 m_1
6	(P_3, P_4) = Take \epsilon (Q_1, Q_2). Q_1 \in {A,B,C} - {P_1,P_2} \land
7     	       	      	   	    	  	Q_2 \in {A,B,C} \land not Q_1 = Q_2
8	 m_2 = Subproblem (Triangles, [geom, euclid, plane, median],
9	       		  	      [geom, euclid, plane, 2circ]) P_3 P_4 m_2

10 in O = Take \epsion O. m_1 \cap m_2

Legend:

1. the steps (breakpoints) where control is passed to the user are: Take and Subproblem (containin further breakpoints)
2. \epsilon is the Hilbert operator of choice.
3. Subproblem is a generalized function call with 2 kinds of arguments:

 * a triple comprising the theory 'Triangles', the specification '[geom, euclid, plane, median]' and the method '[geom, euclid, plane, 2circ]' for the Subproblem
 * the actual arguments for the computational part of the Subproblem, e.g. P_1 P_2 m_1