How to finde postconditions to spark a rubik's cube?

Help
,
1

I programmed a rubik’s cube as a small exercise. So far I got clockwise turns for each site implemented. To make sure that I actually implemented everything right I wanted to spark my code but I got totally stuck on how a post condition would look like for a rubik’s cube.

The current representation for the cube is an array of faces which is an array of squares.

type Square is range 1..6;  --  One of the six "colors" a square can be

type Face is array (1..9) of Square;  --  A side of the cube made of 9 squares

type Cube_Type is array (1..6) of Face;

Cube : Cube_Type := (
   (others => 1),
   (others => 2),
   (others => 3),
   (others => 4),
   (others => 5),
   (others => 6));

Turing the “Upper” side is implemented as

procedure U is
   tmp1 : Square := Cube (2) (1);
   tmp2 : Square := Cube (2) (2);
   tmp3 : Square := Cube (2) (3);

   tmp4 : Square := Cube (1) (1);
   tmp5 : Square := Cube (1) (2);
begin
   Cube (2) (1) := Cube (5) (1);
   Cube (5) (1) := Cube (4) (1);
   Cube (4) (1) := Cube (3) (1);
   Cube (3) (1) := tmp1;

   Cube (2) (2) := Cube (5) (2);
   Cube (5) (2) := Cube (4) (2);
   Cube (4) (2) := Cube (3) (2);
   Cube (3) (2) := tmp2;

   Cube (2) (3) := Cube (5) (3);
   Cube (5) (3) := Cube (4) (3);
   Cube (4) (3) := Cube (3) (3);
   Cube (3) (3) := tmp3;

   Cube (1) (1) := Cube (1) (3);
   Cube (1) (3) := Cube (1) (9);
   Cube (1) (9) := Cube (1) (7);
   Cube (1) (7) := tmp4;

   Cube (1) (2) := Cube (1) (6);
   Cube (1) (6) := Cube (1) (8);
   Cube (1) (8) := Cube (1) (4);
   Cube (1) (4) := tmp5;
end U;

(I know that it looks a bit messy but I double checked the code and tested it already)

I should also add that I use Ada_2022 for the custom 'Image attribute. Makes debugging easier.

How would/should I define the post condition for spark?
Currently I have that the left side is unmoved with Post => Cube (5) = Cube'old (5).
I also need to add the state of all the other squares. How would I tell something like “each third square of one face maps to each third square to another square” in spark?

If you have some comments or recommendations on the way I represent the rubik’s cube or apply movement, I’d be glad to hear them!

2

In fact you can describe all the state changed in the post condition, something like:

procedure U with
   Post => 
      -- Face 1 (Upper face) rotates clockwise
      Cube (1) (1) = Cube'Old (1) (7) and
      Cube (1) (2) = Cube'Old (1) (4) and
      Cube (1) (3) = Cube'Old (1) (1) and
      Cube (1) (4) = Cube'Old (1) (8) and
      Cube (1) (5) = Cube'Old (1) (5) and
      Cube (1) (6) = Cube'Old (1) (2) and
      Cube (1) (7) = Cube'Old (1) (9) and
      Cube (1) (8) = Cube'Old (1) (6) and
      Cube (1) (9) = Cube'Old (1) (3) and
      
      -- Top row of faces 2, 3, 4, 5 cycle
      Cube (2) (1) = Cube'Old (5) (1) and
      Cube (2) (2) = Cube'Old (5) (2) and
      Cube (2) (3) = Cube'Old (5) (3) and
      
      Cube (3) (1) = Cube'Old (2) (1) and
      Cube (3) (2) = Cube'Old (2) (2) and
      Cube (3) (3) = Cube'Old (2) (3) and
      
      Cube (4) (1) = Cube'Old (3) (1) and
      Cube (4) (2) = Cube'Old (3) (2) and
      Cube (4) (3) = Cube'Old (3) (3) and
      
      Cube (5) (1) = Cube'Old (4) (1) and
      Cube (5) (2) = Cube'Old (4) (2) and
      Cube (5) (3) = Cube'Old (4) (3) and
      
      -- All other squares remain unchanged
      (for all F in 2..5 => 
         (for all S in 4..9 => Cube (F) (S) = Cube'Old (F) (S))) and
      Cube (6) = Cube'Old (6);

By the way, it should be possible to reduce the Rubik’s cube problem to a SAT problem (cf this paper)

1 Like
3

Thanks for the answer! The SAT way seams promising and I’ll look into it.

I had thought about copying the code into the post condition but that seamed silly and I scraped that Idea :sweat_smile: That felt like “Statement is true because I say that it’s true”.

I purposefully didn’t look at other implementations because I wanted to feel the joy of figuring it out myself. But that kinda failed when I tried to spark it.

4

Other than postconditions, the only constraints on results are those given in predicates, types and invariants. Anything else potentially mutable (e.g. package state or in out) not described in a postcondition has an unknown state, even if it’s clear to you as a developer that it wasn’t changed.

When writing Anteforth I start with simple predicates and the constrain and refine them as I go.

Since you’re making a Rubik’s cube but modeling each face (vice the individual cube pieces that move), other constraints of a Rubik’s cube should always hold. The corner pieces must have 3 different colors for sides which can physically connect. The edge pieces between two faces must always have 2 different colors which can connect. There are also no duplicate corner or edge pieces. The center faces (along the cube x/y/z axes) are also constrained in their relationship to other going around the cube (my understanding is in the physical puzzle they always maintain their positions relative to each other). Helpers checking these properties help ensure you don’t violate the physical constraints of the cube.

I found a weird tension between SPARK implementation and the modeling itself, but there’s a lot of fun figuring out “I want this property, and I can achieve it this way but not that way.”

1 Like