U·(TP)2 Hacker`s Guide
Contents
1. Name IdPost Y MW S LLstSuffix uffix LXCHARACTERS visible all visible ASCII white alpha amp z W Z digit 0 9 sym visible N alpha U digit LXTOKENS Tok Name alpha AlfDig AlfDig alpha digit Ident IdPost Decor LstS Decor e AlfDig LstSuffix Decor Roots Roots Name Num digit digit Symbol symN White sym O 11 SNWORDS Q Binop n Name UN f lt gt se farsa ad facet v Variable c Constant Q Binder Uy z 0 Nx y true false 0 1 2 V the forall exists exists1 Forall Exists WWW HV UUU YU TEPSYNTAX pe PredExpr tm lt I pe 1 tm tm Term f G tm with precedences f Factor b Qqs I pe pe b Base c mn v se le de he 1 T se SEmpr Oen Las EI pel pe Y Cmer y he HEspr Upe ly Lv LV pel pe IP le LExpr Upe Ps de DExpr LUpe 11 pne tty LE Lang user specified T Type see elsewhere qs QVars n v me MElem pe gt pe sb Subs CUA PEE nz1 12 TEPLSYNTAX pe PredExpr im Term f Factor b Base se SExpr sec SExprCont mec MExprCont le LExpr lec LExprCont qs QVar2. documentation are written and organised At present this document is a very rough draft 1 3 Gotchas This at the moment is a unstructured list of things we feel you really ought to know before you start hacking e The datatypes Expr and Pred in src Datatypes lhs have focus vari ants used in proofs These no longer use a knot tying style see src Focus 148 So this gotcha in earlier versions of this guide is no longer an issue Chapter 2 Program Structure 2 1 Overview The sources for U TP comprise a very large collection of IXTEX sources and Haskell Literate Scripts which are themselves also valid IATEX The directory folder structure has been designed to support ease of develop ment for the main development environment namely WinEdt MikTeX ghci on Windows currently Windows 8 2 2 Directory Structure The top level contains all the IA3TEX master documents currently including UTP2 MAIN tex U TP sources and documentation UTP2 Hacking MAIN tex This document UTP2 Reference MAIN tex Reference manual UTP2 User Manual MAIN tex User Guide Almost all other files present at this level should be considered as junk even if tracked by Mercurial This will be tidied up at some future date Subdirectories are organised as follows src Haskell source files as well as MS DOS batch files bat for building under Windows doc Mainly ATEX files giving documentation of various forms as well as text files t
3. U TP Hacker s Guide Andrew Butterfield November 21 2013 Contents 1 Introduction 2 L Whati ULP Sus a5 quuin Ad a pu ORE awe 2 1 2 Structure of This Document 2 Lot Gxobchas 23 t dA ik kh lE Bee qu uk as 2 2 Program Structure 3 24 OVerview mosse a ee EAL DA Uy IUE OS GUESS 3 2 2 Di rectory SUructure zu s rug ROV y wee eges 3 2 3 Literate File Structure aoaaa 4 2 3 1 DA TP Source Example 22 oni od ea A 6 24 DEP Distribution Structure 6 241 README AKT gt o 605 fate i ESSA Asa 7 242 SGOPVINGAXT ern A oo o ee Al We der ub de 8 243 INSTALL AX 3k nU RRSP Ee ede A dp be wed 9 2 4 4 MANIFEST txt 2 o es 10 3 Odds and Ends 11 3 1 Parser Implementation eee o 11 3 1 1 Type Expression Predicate Parser Grammar 11 3 2 MacOS X ScreenShot Renaming 14 Chapter 1 Introduction 1 1 What is U TP U TP is a theorem proving assistant for Hoare and He s Unifying Theories of Programming UTP HH98 It was developed as a tool to support foundational work in the UTP that is the development of UTP theories A user friendly graphical user interface GUI has been designed into the tool from the start 1 2 Structure of This Document This is the Hacker s Guide for U TP It gives an overview of how the program and
4. ample begin code module Example where import Utilities end code subsubsection Intro We can have a suitably mathematical comment sigma circ sigma mathsf id and then some code begin code Sigma negate end code When typeset this results in 2 3 1 U TP Source Example module Example where import Utilities Intro We can have a suitably mathematical comment o oc id and then some code sigma negate 2 4 U TP Distribution Structure At present Unix and Mac OS X users have to build from source and at present we do not have proper makefiles or install scripts For windows users we package up a binary release Below are listing of all the relevant installation text files 2 4 1 README txt UTP2 is a Theorem Proving Assistant for Unifying Theories of Programming Copyright C Andrew Butterfield 2007 2012 School of Computer Science and Statistics Trinity College University of Dublin Ireland See COPYING txt for licence and warranty information 2 4 2 COPYING txt This work is released under GPL version 2 see GPL2 txt for details of the licence and warranty It incorporates material from Mark Utting s jaza animator licensed under GPL2 It also uses the Parsec library distributed with Haskell see PARSEC LICENCE txt for details and the relevant warranty It also uses the wxHaskell library distributed with Haskell see WXWINDOWS LICENCE txt for details an
5. d the relevant warranty The software includes sounds from freesound org all distributed under the Creative Commons Sampling Plus 1 0 license viewable at http creativecommons org licenses sampling 1 0 Saoithin note wav derived from Chipii6 wav by HardPCM Saoithin alert wav derived from Chip073 by HardPCM Saoithin cheer wav derived from dramatic drum roll wav by ingsey101 Saoithin scream wav derived from crash wav by sageturtle 2 4 8 INSTALL txt INSTALLATION INSTRUCTIONS Binary install for Windows 1 Unpack ZIP archive to where you want application to live 2 Run executable it should set up required directories and files LaTeX packages required to render code documentation saoithin included amssymb amsmath verbatim tikz graphicx not included but should be in any standard distribution mathpartir not included available from http pauillac inria fr remy latex 2 4 4 MANIFEST txt Windows Manifest UTP2 exe saoithin sty wxc msw2 8 10 0 11 1 2 d11 README txt INSTALL txt MANIFEST txt COPYING txt WXWINDOWS LICENCE txt GPL2 txt PARSEC LICENCE txt jaza COPYING txt Saoithin alert wav Saoithin note wav Saoithin cheer wav Saoithin scream wav UTP2 Reference DRAFT pdf UTP2 User Manual DRAFT pdf 10 Chapter 3 Odds and Ends 3 1 Parser Implementation 3 1 1 Type Expression Predicate Parser Grammar characters all invisible ASCII characters j Name Ident Num Symbol
6. o do with installation It has a couple of sub directories to manage certain types of documentation formal mainly formal definitions of aspects of the logic images images obviously papers sources for conference journal papers about U TP styles IATEX style files currently ignored screenshots screen shots of the tool in action arranged in topic sub directories batch Created by someone from a unix background to hold bat files Deprecated unused will probably disappear licence Licensing files orphans unwanted and unloved also likely to vanish resource mainly sound and help files The help file with the long unpronounceable name has been subsumed into the relevant code and is no longer required test test stuff currently unused but we will probably flesh this out at some stage thlib This is where we build U TP theories to drive and test the development and most of which will become part of a standard theory library release www Stuff for the release website 2 3 Literate File Structure All the Haskell source files are literate scripts lhs extension that are them selves valid TEX files in which the Haskell source is enclosed in begin code end code environments The code environment is defined in the style file doc saoithin sty We do not use bird tracks or 1hs2tex nor do we use Hackage Haddock in any way An example of some lhs source is below subsection UTP2 Source Ex
7. oRename String gt Int FilePath gt IO doRename title n oldpath renameFile oldpath title title display 4 n png display w n replicate w length s 0 s where s show n 14 Bibliography HH98 C A R Hoare and Jifeng He Unifying Theories of Programming Prentice Hall 1998 15
8. s he HExpr hec HExprCont Lang tm lt 1 pe 1 tm f G tm with precedences b f epu pw SEE 26941 E peo se De Ehe Q qs I pe pe E s de 2p Y pe sec aV pe C pe F PS pet P et pe mec P pe gt pe mec pe lec VY 77 gu T 777 as T n v FP pe hec v V pe O pe 3 Sto pet p ec user specified 13 3 2 Mac OS X ScreenShot Renaming This is standalone code intended for use on Mac OS X to rename screenshots from that platform module OSXRename where import Data Char import System I0 import System Directory import System FilePath Posix what putStrLn doit IO O doit ssRenameFiles isOSXNewScreenShot isOSXNewScreenShot path takeExtension path png amp amp take 11 path Screen Shot ssRenameFiles FilePath gt Bool gt IO O ssRenameFiles newShot do paths lt getDirectoryContents putStrLn nBEFORE putStrLn unlines paths putStr Starting Number negative to abort txt lt getLine let firstNo read txt Int if firstNo O then putStrLn No files renamed else do putStr Screenshot Series Title filename characters only title getLine createDirectoryIfMissing True title mapM doRename title zip firstNo filter newShot paths putStrLn Files renamed paths lt getDirectoryContents title putStrLn nAFTER putStrLn unlines paths d
Download Pdf Manuals
Related Search