4 ms·
Decision Tables[1] is probably the simplest formal method, i.e. instead of writing imperative nested if and switch/case statements, your provide a declarative s
by nivertech 5y ago
Decision Tables[1] is probably the simplest formal method, i.e. instead of writing imperative nested if and switch/case statements, your provide a declarative solution.
But IMO the most useful formal method in Software Engineering is modeling your code as an FSMs, for example using StateCharts UML notation [2,3].
That way even junior developers can reason about complex realtime systems.
Next close come Algebraic Type Systems, but they're usually not available in mainstream PLs.
Unfortunately Formal Specification/Verification tools like TLA+, Alloy, etc. are less practical for most real life projects.
--
[1] https://en.wikipedia.org/wiki/Decision_table https://en.wikipedia.org/wiki/Decision_table
[2] https://en.wikipedia.org/wiki/UML_state_machine https://en.wikipedia.org/wiki/UML_state_machine
[3] https://en.wikipedia.org/wiki/State_diagram#Harel_statechart https://en.wikipedia.org/wiki/State_diagram#Harel_statechart
- brenainn 5y agoState machines are handy, and along with modelling they can be implemented directly. A simple implementation is you define the possible states for your application, or module or whatever, and the valid transitions from state to state. You assign the new state when the state should transition, and this assignment is wrapped by some simple check that the transition is valid. If not, throw an error, or handle it, etc. The state path can also be logged to aid with debugging. I've found it invaluable in building web apps, finding odd things not caught in traditional testing e.g. like cases of trying to transition from the current state to the same state.
- rowanG077 5y agoWhat are Algebraic Type Systems? Google only gives me the run of the mill algabraic data types.
- nivertech 5y agoI mean type systems used in ML family PLs. They're a static type systems based on algebraic data types. https://en.wikipedia.org/wiki/Algebraic_data_type https://en.wikipedia.org/wiki/Algebraic_data_type
- nivertech 5y agoProperty-Based Testing (PBT) is another pragmatic formal method that can be used in combination with more traditional example-based TDD.