We don't have a formal functional specification for the SeqTools programs; instead, required behaviours are defined by means of a test plan, which specifies a set of testable actions and their expected outcomes. The test plan is an OpenOffice spreadsheet. To get a general overview of program behaviour, see the user documentation.