Solving hybrid constraints to validate specification requirements of a software module

A system comprising:

• a memory comprising instructions executable by one or more processors;
• and
• one or more processors coupled to the memory and operable to execute the instructions, the one or more processors being operable when executing the instructions to:
• analyze one or more first numeric constraints and one or more first string constraints associated with a software module, wherein:
• the software module comprises:
• one or more numeric variables;
• one or more string variables;
• one or more first operations that apply to specific ones of the numeric variables and produce numeric or string results;
• and
• one or more second operations that apply to specific ones of the string variables and produce numeric or string results;
• the first numeric constraints apply to specific ones of the numeric variables;
• and
• the first string constraints apply to specific ones of the string variables;
• infer one or more second numeric constraints applying to specific ones of the string variables;
• infer one or more second string constraints applying to specific ones of the numeric variables;
• represent each one of the first and second numeric constraints with an equation;
• represent each one of the first and second string constraints with a finite state machine;
• and
• validate the software module with respect to one or more requirements associated with the software module by attempting to solve for a solution comprising one or more values for specific ones of the numeric and string variables that satisfies all the first and second numeric constraints, all the first and second string constraints, and all the requirements,
• wherein attempt to solve for the solution that satisfies all the first and second numeric constraints, all the first and second string constraints, and all the requirements comprises:
• iteratively try different possible values for the numeric and string variables and test whether the possible values together produce a solution that satisfies all of the first and second numeric constraints, the first and second string constraints, and the requirements until a solution is found, the first and second numeric and string constraints are determined to be unsatisfiable, or a number of the iterations reaches a threshold;
• and
• if a solution is found, then output the values for the numeric and string variables.

A computer-readable non-transitory storage media embodying software operable when executed by one or more computing devices to:

• analyze one or more first numeric constraints and one or more first string constraints associated with a software module, wherein:
• the software module comprises:
• one or more numeric variables;
• one or more string variables;
• one or more first operations that apply to specific ones of the numeric variables and produce numeric or string results;
• and
• one or more second operations that apply to specific ones of the string variables and produce numeric or string results;
• the first numeric constraints apply to specific ones of the numeric variables;
• and
• the first string constraints apply to specific ones of the string variables;
• infer one or more second numeric constraints applying to specific ones of the string variables;
• infer one or more second string constraints applying to specific ones of the numeric variables;
• represent each one of the first and second numeric constraints with an equation;
• represent each one of the first and second string constraints with a finite state machine;
• and
• validate the software module with respect to one or more requirements associated with the software module by attempting to solve for a solution comprising one or more values for specific ones of the numeric and string variables that satisfies all the first and second numeric constraints, all the first and second string constraints, and all the requirements,
• wherein attempt to solve for the solution that satisfies all the first and second numeric constraints, all the first and second string constraints, and all the requirements comprises:
• iteratively try different possible values for the numeric and string variables and test whether the possible values together produce a solution that satisfies all of the first and second numeric constraints, the first and second string constraints, and the requirements until a solution is found, the first and second numeric and string constraints are determined to be unsatisfiable, or a number of the iterations reaches a threshold;
• and
• if a solution is found, then output the values for the numeric and string variables.

A system comprising:

• means for analyzing one or more first numeric constraints and one or more first string constraints associated with a software module, wherein:
• the software module comprises:
• one or more numeric variables;
• one or more string variables;
• one or more first operations that apply to specific ones of the numeric variables and produce numeric or string results;
• and
• one or more second operations that apply to specific ones of the string variables and produce numeric or string results;
• the first numeric constraints apply to specific ones of the numeric variables;
• and
• the first string constraints apply to specific ones of the string variables;
• means for inferring one or more second numeric constraints applying to specific ones of the string variables;
• means for inferring one or more second string constraints applying to specific ones of the numeric variables;
• means for representing each one of the first and second numeric constraints with an equation;
• means for representing each one of the first and second string constraints with a finite state machine;
• and
• means for validating the software module with respect to one or more requirements associated with the software module by attempting to solve for a solution comprising one or more values for specific ones of the numeric and string variables that satisfies all the first and second numeric constraints, all the first and second string constraints, and all the requirements,
• wherein attempting to solve for the solution that satisfies all the first and second numeric constraints, all the first and second string constraints, and all the requirements comprises:
• means for iteratively trying different possible values for the numeric and string variables and testing whether the possible values together produce a solution that satisfies all of the first and second numeric constraints, the first and second string constraints, and the requirements until a solution is found, the first and second numeric and string constraints are determined to be unsatisfiable, or a number of the iterations reaches a threshold;
• and
• if a solution is found, then means for outputting the values for the numeric and string variables.