CS427: Software Engineering IMidterm examProject groupsProject gradingClassic software engineering phasesWhy phases?Other forms of decompositionSpecificationNotationsWhy formal languages?Credit cardData and operationsProperties of operationsQuestion not on MEExtending operationsFirst approachSecond approachSlide 18ComparisonDesign and specificationExecutable specifications (1)Executable specifications (2)Story about AdaStory about concurrencyConclusionNext time1CS427:Software Engineering IDarko Marinov(slides from Ralph Johnson)CS427 13-2Midterm examYour opinion?Hard/easy? Long/short? Surprising/not?Reading books is importantDid you like format of questions? T/F?Grades will be on Wiki by Friday, Oct 13If you have questions, please let us knowIf you think we erred, please let us knowCS427 13-3Project groupsOnly groups 8 and 27 have 8 students so far8 students is ideal; it may be 7 or 9 at the endProject fair5pm on Friday, Oct 13, room TBA (Wiki)You should come ifYou’re a representative of a group with <8 studentsYou’re still looking for a groupEach representative will give a brief presentationHW2 (due Oct 24) asks for details of your projectCS427 13-4Project gradingYou are graded on how well you follow your process (you decide XP or RUP)You must know itYou must follow itYou must prove you follow itMake a log of what you do every dayProject is 35% of gradeHWs help you to make progress on the projectCS427 13-5Classic software engineering phasesPut them in correct order: code, design, maintenance, requirements, specification, test [ME: almost all correct answers]We covered requirements and some designToday: specifications (specs)Do customers and users need to understand requirements (or specs)? [ME: many wrong]CS427 13-6Why phases?Break big job into smaller stepsLet people specializeProvide check-pointsProvide early feedback Provide multiple viewsCS427 13-7Other forms of decompositionModules/componentsFor each module, follow req-spec-design-code-test cycleFeaturesFor each feature, follow req-spec-design-code-test cycleCS427 13-8SpecificationDefine system as a set of data items and operations on that dataSpecification is set of properties of data and operations Example: bank balance is never negativeFormal spec: “forall a: Account. a.balance ≥ 0”CS427 13-9NotationsEnglishEasy to readHard to analyzeProgramming languageEasy for programmers to readOften not powerful enoughSpecial (formal) specification languagesWe don’t teach much on this topic in CS427CS427 13-10Why formal languages?Can describe many artifacts (specs, designs, requirements) [ME: many correct answers]Documentation (precise, unambiguous)Enables (automatic!) machine reasoningInformal: “everybody likes a winner”?1)exists w: Winner. exists p: Person. p.likes(w)2)exists w: Winner. all p: Person. p.likes(w)3)all p: Person. exists w: Winner. p.likes(w)4)all p: Person. all w: Winner. p.likes(w)CS427 13-11Credit cardA credit card has a balance that is the sum of all charges minus the sum of all payments. If the balance is not paid within 20 days of billing, 1% of the unpaid balance is charged as interest. Each credit card has a particular day on which it is billed each month. Customers cannot charge if the charge would put balance over the limit. [Data and operations?]CS427 13-12Data and operationsCredit card hasbalancelimitbilling dayOperations on credit cardpay(amount)charge(amount)CS427 13-13Properties of operationsCan’t say balance equals sum of all charges minus sum of all payments due to interestInvariant: what holds in all statesCan say “c.pay(a).balance = c.balance - a”Postcondition: what operation establishesCan say “if c.balance + a < c.limit then c.charge(a).balance = c.balance + a”Precondition: what operation assumesCS427 13-14Question not on MEConsider binarySearch(int[] a, int v) methodInput: array and a value to search forOutput: position of value in the arrayUses binary searchWhat should be precondition?a is sorted T/Fa is not null T/FCS427 13-15Extending operations “If the balance is not paid within 20 days of billing, 1% of the unpaid balance is charged as interest.”CS427 13-16First approachAdd “unpaid balance” to a credit cardunpaidBalance = balance on billing datepayments get subtracted from unpaidBalance20 days after billing, compute interest and charge itCS427 13-17Second approachAdd date to payments and chargesOperations on credit cardpay(amount, date)charge(amount, date)Credit card hasbalance, limit, billing dayset of paymentsset of chargesCS427 13-18Second approachFor each credit cardbalance(date) = (sum a for d<=date of charges(a,d)) –(sum a for d<=date of payments(a,d))There is a c in charges(a, billingDate + 20) wherec.balance(billingDate) –sum a for d<=date of charges(a, d)CS427 13-19ComparisonFirst approachMore like programmingMore standard notationLonger specsSecond approachShorter, more abstract, easier to reason aboutMore to learnPersonal experience: Java vs. AlloyCS427 13-20Design and specificationSpecification needs to know dataSpecification needs to be structuredMust design module interfacesSpecification is usually the design of the “entities”CS427 13-21Executable specifications (1)Some very high-level programming languages can be used to write specsProlog (Hamlet and Maybee, you don’t need details)LispSmalltalkMaude (several courses on formal methods)CS427 13-22Executable specifications (2)Write and test specificationRewrite in efficient languageWrite and test specificationRewrite to be more efficientCS427 13-23Story about AdaAda - language invented by military project around 1980Specification, verification suiteFirst Ada compiler written in SetL “Set Language”Slow, but tested spec and verification suiteMoral: executable specifications are usefulCS427 13-24Story about concurrencySystem for downloading data from cash registers (Prof. Johnson’s experience)Frequent deadlockAfter fourth attempt, developed formal specification and derived a designMoral: formal techniques can solve hard problemsAutomated analysis: model checkingCS427 13-25ConclusionSpecifications can beInformal or