animation-tutorial

Description

COMP4603/7606 High Integrity Software DevelopmentTutorial — Sum Type Checker and PossumIntroductionThistutorialhandoutwillassistyouwithrunningtheSumtypecheckerandPossum. Itistheintentionthat this tutorial should be sucient for you to use the type checker and Possum without havingto read any other documentation. However, if you are interested, the following, more substantialdocumentation is also available from the course web page. Possum user guide (37 pages): the most relevant parts of the user guide have been used in thistutorial. Sum reference manual (158 pages): complete reference manual for the Sum language. Copy of the technical report “Requirements Engineering and Veri cation using Speci cationAnimation” (14 pages), which brie y describes Possum (mostly a subset of what is in the userguide) and some of the applications it has been used in.Sum type checkerThe Sum type checker is stored in the comp4603 account on the student network. To run the Sumtype checker, you must rst ensure that your environment is set up correctly. You can do this byadding the commands from the le~comp4603/sumenvto your .profile or by copying this le to your area and running. sumenvYou can then execute the command runsum to invoke a GUI interface that allows you to edit Sum les and to run the Sum type checker. To typecheck a Sum speci cation with the GUI, you can clickthe Run button (button with a running person icon on it). Make sure the appropriate options areset ...

Informations

• Publié par: Jarak
• Nombre de lectures: 6
• Langue: English

Extrait

COMP4603/7606 High Integrity Software Development Tutorial — Sum Type Checker and Possum

Introduction This tutorial handout will assist you with running the Sum type checker and Possum.It is the intention that this tutorial should be sufficient for you to use the type checker and Possum without having to read any other documentation.However, if you are interested, the following, more substantial documentation is also available from the course web page. •Possum user guide (37 pages):the most relevant parts of the user guide have been used in this tutorial. •Sum reference manual (158 pages):complete reference manual for the Sum language. •Copy of the technical report “Requirements Engineering and Verification using Specification Animation” (14 pages), which briefly describes Possum (mostly a subset of what is in the user guide) and some of the applications it has been used in.

Sum type checker The Sum type checker is stored in thecomp4603account on the student network.To run the Sum type checker, you must first ensure that your environment is set up correctly.You can do this by adding the commands from the file ~comp4603/sumenv to your.profileor by copying this file to your area and running . sumenv You can then execute the commandrunsumto invoke a GUI interface that allows you to edit Sum files and to run the Sum type checker.To typecheck a Sum specification with the GUI, you can click theRunbutton (button with a running person icon on it).Make sure the appropriate options are set under theRun Optionsmenu:Syntax Checkfor just a syntax check, and bothSyntax Check andType Checkfor a syntax and type check.The GUI also provides a list of all the symbols in the ASCII syntax of Sum.To view this list, selectDisplay Reserved Wordsfrom theDisplaymenu. Alternatively, you can use the stand-alone Sum typechecker by using the commandtcsum1a file. For foo.sum, you should execute the command tcsum1 foo.sum for just a syntax check, and tcsum1 -T foo.sum for a syntax and type check.

Possumexamples

The directory

~comp4603/assign2

contains an example Sum specification (IntSet.sum) and two Possum scripts (IntSet.scriptand examples.scriptTo access these example specification) with a number of simple queries in them. and scripts, it is probably best to change directory to where they live before you invoke Possum.The directory

~comp4603/possum/Examples

also contains many other examples (some of which are referenced in the Possum user guide), but please be aware that some of these may contain errors.

1

Possum invocation The Gui interface to Possum is started by running the script: Possum As Possum starts, a Possum Interpreter window should pop up containing a commandline prompt.

Expression enumeration Possum simply enumerates and grounds Z expressions.Type a few simple Z expressions at the prompt. 1. Forexample, type: 11 + 5 and key Control-Return to send it to Possum. 2. Someexpressions which appear already to be ground are put into a canonical form: { 3, 2, 4 } (key Control-Return ) 3. AskPossum to enumerate a set comprehension: { x, y : 0 .. 200 | x * 13 = y * 11 } (key Control-Return ) 4. Key Control-Up to edit a previous input: { x, y : 0 .. 200 | x * 13 = y * 11 @ x * y } (key Control-Return ) 5. Andagain: { x, y : 0 .. 200 | x * 13 = y * 11 @ x * y / 143 } (key Control-Return ) 6. Declarea schema right there at the commandline by typing the following: schema S is dec n, d : 2 .. 100 pred n < d; d mod n = 0 end S (key Control-Return ) Possum responds withYesto declarations it has used to expand its environment. 7. NowthatShas been declared, it can be used in the ways Z allows.For example, type: S (key Control-Return ) By default Possum provides some satisfying binding ofS. 8. UseSFor example ask Possum for allas a type.wof typeS. { w : S } 9. Editthe last query.We’re only interested in thedfields. { w : S @ w.d } 10. Theseare the non-primes.Subtract them from(2 .. 100)to get the primes: (2 .. 100) diff { w : S @ w.d }

2

Saving and rerunning scripts

Possum can re-run previously saved sessions interactively.

1. SelectSave...from theFilesmenu and provide a file name.Obviously you will need permission to write the file.Somewhere under your home directory perhaps, or in/tmp. 2. Onceyou have successfully saved the session, selectQuit!from thePossummenu. 3. StartPossum again. 4. SelectOpen recentfrom theFilesmenu and choose the name of the file to which you saved the last session.Alternatively, selectOpen ...from theFilesmenu and explore to find the saved session file. 5. ASession File Buffer should have opened.Click the button markedSenda few times and watch as the queries are re-issued to the Possum Interpreter window. 6. Selectan arbitraryRedquery in the Session File Buffer using MouseButton-1.It should turn Blue. Clickthe button markedSend. 7. Clickthe button markedSend Rest. 8. SelectResetfrom thePossummenu or quit and restart. 9. SelectRun Script ...from theFilesmenu and run some.scriptscript files.SelectResetfrom thePossummenu between each run.

Reading Sum specifications and state machine tracing

Possum can be used to load a Sum specification and to step through successive states of a state machine.

1. SelectOpen ...from theFilesmenu and open the file namedIntSet.sum. Notethat this opens the Sum specification in a separate window, but does not read in the specification in Possum. 2. To read in the specification, selectRead ...from theFilesmenu and read in the file named IntSet.sum. 3. Possumhas a notion of a “current module” and to be able to work with theIntSetmodule, you must make it the current module by typing: param currentmodule IntSet into the Possum Interpreter window (or by selectingIntSetas the current module under the Parameters ...option of theDialogsmenu). 4. Whenstepping through a state machine, we often want to see how the state is updated after various operations.To display thestateschema, type display state into the Possum Interpreter window.Note that the state variables are unbound because no operation has been invoked yet. 5. Invokethe schemainitby typing: init into the Possum Interpreter window.The bindings of the variables in the schemastatehave now been updated.Note that these correspond to those of their dashed counterparts in a satisfying binding of the schemainitwhich has just been invoked.Possum has overwritten the undashed bindings with the values provided by the dashed bindings because the parameterautocompose is set by default (see section on Parameters below). 6. Invokethe schemaaddby typing:

3

add { 1/x? } into the Possum Interpreter window.Note again that the state has been updated. 7. Key Control-Up Control-Return to invoke a second call toaddwith the same parameter.Note that Possum responds withno solutionin this case, because theaddoperation does not allow an element to be added to the set twice. 8. Useschema composition to make two calls toaddin a single Possum query by typing: add { 2/x? } s_compose add { 3/x? } into the Possum Interpreter window. 9. Key Control-Up to undo the last command that was just invoked.Note that the state reverts back to what it was before the last Possum command. 10. Tocheck the outputs of schemas such asisMember, you should use isMember { 1/x? } >> which shows the value of the output variables on a separate line. Note that in theory you should also be able to use isMember { 1/x? } without the>>at the end, which should disply the output as part of the input and state variables. However, there is a bug in Possum, which means that if you use this second form, it permanently binds the output variable to the value returned by this query.This in turns mean you cannot call the same method again if it would return a different value. Theupshot of this is that you should always include the>>at the end of a query that includes output variables. 11. Youcan of course use scripts to save and rerun queries on Possum modules as well.SelectReset from thePossumSelectmenu or quit and restart Possum.Run Script ...from theFilesmenu and run the script namedIntSet.scriptin thecomp4603/assign2directory.

Aborting queries

In some cases, it may take Possum a very long (or even infinite) amount of time to return from a query. Whenthis happens, you can interrupt the query by selectingAbortfrom thePossummenu or by clicking the button markedSTOPor by keying Control-c into the Possum Interpreter window. Note that when this happens, this does not necessarily (but could) indicate an error in the specification. Of course, this means it is then up to you to decide whether the specification needs to be fixed because it contains an error, to be rewritten so that you can animate it with Possum, or to be left as is because it is correct (in that case, you will have to accept that this part of the specification cannot be tested using Possum).

Parameters Parameters may be set using theparamcommand or by selectingParameters ...from theDialogs menu. Theparameters that you may wish to use are as follows:

currentmodule May be assigned the name of any imported module.An unparameterised module is implicitly imported upon declaration.The notion of a current module is used by Possum in several ways. 1. All declarations are made ‘into’ the current module.Declarations of new modules are nested within the current module and as such are implicitlyimported, but not madevisible. 2. Modulecomposition is performed with respect to the state schema of the current module. 3. Name qualification is done with respect to the current module.Setting the parameter currentmodule toMfor example, makes allM’s symbols visible (M.xmay be referenced simply byx).

4

autocompose May be assignedonoroff. If this parameter is set toon, Possum instantiates any state variablexin the current module to 0 0 the value of the variablexany such. Ifxis not bound, no instantiations occur.Without this metalogical autocompose function, variable bindings cannot change and a state machine would not be allowed to evolve.

maxint 31 May be assigned any positive integerN<2 . As far as Possum is concerned, the typeZis equivalent to −MAXINT. .MAXINT and the typeNis equivalent to 0. .MAXINT whereMAXINTis the current value of this parameter. printsequences May be assignedonoroff. If this parameter is set toon, total functions on the domain (1. .n), wherenis some positive integer, will be displayed as sequences.For example, the set {17→c,27→b,37→a} will be displayed as hc,b,ai

printbags May be assignedonoroff. If this parameter is set toon, functions to positive integers will be displayed as bags.For example, the set {a7→2,b7→3,c7→1} will be displayed as [a,a,b,b,b,c]

printmaplets May be assignedonoroff. If this parameter is set toonFor example,, ordered pairs will be printed as maplets.

{(0,10),(1,9),(2,8),(3,7),(4,6),(5,5),(6,4),(7,3),(8,2), (9,1),(10,0)}

will be printed as

{07→10,17→9,27→8,37→7,47→6,57→5,67→4,77→3, 87→2,97→1,107→0}

This parameter is set tooffby default.

queryreflection May be assignedonoroff. If this parameter is set toon, a window is popped up after query with all schemas dereferenced and unfolded and all ing the pointer over subterms and variables displays their subterms are coloured to indicate whether they have been

5

each successful query displaying that schema operations performed.Mov- particular simplifications.Predicate simplified totrueorfalse.