A First Step in the Design of a Formally Verified Constraint-Based Testing Tool: FocalTest