I think for application developers, a big potential use of SMT is checking rule equivalences. If we have set of business rules A and want to add rule z, what’s an input that satisfies A but not A+z? I’ve toyed a bit with this but haven’t tried it in anger yet, though I know at least one person who successfully did it.
One similar use case I often come across is whether a given SQL Where clause statement ‘covers’ several others.
This often comes up in caching and ETL.
In caching – you want to know if a cache that was created with where.clause.1 would contain items for where.clause.2 and where.clause.3 .
The same with ‘request caches’. Where an a cache for API.call.1 will contain a superset of entries for API.call.2 or.3
–
In ETL this comes in many batch jobs. Batch jobs are usually limited to a subset of data, and the question often about whether the ‘data perimeter’ of batch job 1 contains subsets for jobs 2 and 3.
–
Properly identify subsets of data retrieved by APIs or by SQL reduces the need for ‘duplicates’.
I think for application developers, a big potential use of SMT is checking rule equivalences. If we have set of business rules A and want to add rule z, what’s an input that satisfies A but not
A+z? I’ve toyed a bit with this but haven’t tried it in anger yet, though I know at least one person who successfully did it.One similar use case I often come across is whether a given SQL Where clause statement ‘covers’ several others.
This often comes up in caching and ETL.
In caching – you want to know if a cache that was created with where.clause.1 would contain items for where.clause.2 and where.clause.3 .
The same with ‘request caches’. Where an a cache for API.call.1 will contain a superset of entries for API.call.2 or.3
–
In ETL this comes in many batch jobs. Batch jobs are usually limited to a subset of data, and the question often about whether the ‘data perimeter’ of batch job 1 contains subsets for jobs 2 and 3.
–
Properly identify subsets of data retrieved by APIs or by SQL reduces the need for ‘duplicates’.