CSE P503: Principles of Software Engineering David Notkin

CSE P503: Principles of Software Engineering David Notkin

CSE P503: Principles of Software Engineering David Notkin Autumn 2007 Requirements and Specifications or You can't always get what you want But if you try sometime, yeah, You just might find you get what you need! --Jagger & Richards When I want to know what France thinks, I ask myself. --de Gaulle If you dont know where youre going, it doesnt matter how you get there. --Anonymous Tonight: an experiment A few interludes on questions and concerns that have been raised by the one-minute papers, email, etc.

What is an engineer? An empirical software engineering research result A cool tool UW CSE P503 David Notkin Autumn 2007 2 Requirements & specification More software systems fail because they dont meet the needs of their users than because they arent implemented properly Boehm Verification: Did we build the system right? Validation: Did we build the right system? UW CSE P503 David Notkin Autumn 2007

3 Our plan of attack: this week An overview of the key problems in requirements and specification A brief history in proving programs correct An expected panacea for software that didnt pan out But has provided some benefits Is a basis for model-based specifications (below) A look at formal specifications, with a focus on two forms Model-based specifications (Z) Overview of state machine based specifications UW CSE P503 David Notkin Autumn 2007 4

Our plan of attack: next week Analysis of state machine based specifications (model checking) A brief overview of requirements engineering issues MAYBE: Michael Jackson on video: The World and the Machine UW CSE P503 David Notkin Autumn 2007 5 Non-functional requirements Were simply going to ignore non-functional requirements Performance, ease of change, etc.

Im not proud of this, but there is relatively little known about this issue Worthwhile concrete discussion: should an interfaces specification (documentation) specify the performance of the operations? Pro: Sure, its a key property (and people will find it out anyway) Con: No way, since Im supposed to be able to change an implementation as long as it behaves the same Topic worthy of a research paper UW CSE P503 David Notkin Autumn 2007 6 Dogs and shoes x (OnEscalator(x)OnEscalator(OnEscalator(x)x) y (OnEscalator(x)PairOfShoes(OnEscalator(x)y) IsWearing(OnEscalator(x)x,y)) x (OnEscalator(x)(OnEscalator(x)OnEscalator(OnEscalator(x)x) IsDog(OnEscalator(x)x))

IsCarried(OnEscalator(x)x) Do dogs have to wear shoes? What are the types of the variables? What are dogs? What does it mean to wear shoes? Designation: a recognition rule for recognizing some class of phenomenon that you could observe in a domain. [M. Jackson] Why do the formalizations say dogs are carried and shoes are worn while the signs say must be? The formalizations are in the indicative mood: statements of fact The signs are in the optative mood: statements of desire Separating facts from desired behavior can reduce confusion UW CSE P503 David Notkin Autumn 2007

7 Calvin and Hobbes: on designations Explain Newtons First Law of Motion in your own words. I love loopholes! UW CSE P503 David Notkin Autumn 2007 8 Pick your poison Specification languages that are closer to the user

decrease the change of building the wrong system But increase the chance of building the system wrong And specification languages that are closer to the program do the opposite Specification Why might you pick one over the other? Program UW CSE P503 David Notkin Autumn 2007 9 Formalism

In the mid-1960s, there was a set of software research today we call it programming methodology that was intended (in my view) to solve two problems Decrease ambiguity through the use of mathematics to specify programs Allow us to prove programs correct by showing that a program satisfies a formal specification Turing Awards in this area include: Dijkstra (1972), Floyd (1978), Hoare (1980), Wirth (1984), Milner (1991), Pnueli (1996) UW CSE P503 David Notkin Autumn 2007 10 Dont be confused I dont believe that this is a practical approach in most situations

It may be applicable in some situations But its a useful basis for some other work And the historical context is important And the technical material is of value UW CSE P503 David Notkin Autumn 2007 11 Interlude: what is engineering? Merriam-Webster 2 a: the application of science and mathematics by which the properties of matter and the

sources of energy in nature are made useful to people b: the design and manufacture of complex products UW CSE P503 National Academy of Engineering Engineering has been defined in many ways. It is often referred to as the application of science because engineers take abstract ideas and build tangible products from them. Another definition is design under constraint, because to engineer a product

means to construct it in such a way that it will do exactly what you want it to, without any unexpected consequences. David Notkin Autumn 2007 12 Engineer The title engineer is controlled by countries and, within the U.S., by states, in various ways In the U.S., with some differences between states, Professional

Engineers are registered or licensed, based on a degree from an accredited four-year university engineering program passing a standard Fundamentals of Engineering (FE) test on basic engineering principles gaining engineering experience, of about four years, under the supervision of a Professional Engineer passing the Principles and Practice in Engineering (PE) test in a specific engineering discipline (plus engineering ethics) A Professional Engineer is authorized to "stamp" engineering documents for a studies, designs, etc. This formally takes legal responsibility Some states license per discipline, others in general, but UW CSE P503 David Notkin Autumn 2007 13 Software engineer

Some states protect all engineer titles, some only Professional Engineer Washington State RCW 18.43.010 In order to safeguard life, health, and property, and to promote the public welfare, any person in either public or private capacity practicing or offering to practice engineering or land surveying, shall hereafter be required to submit evidence that he is qualified so to practice and shall be registered as hereinafter provided; and it shall be unlawful for any person to practice or to offer to practice in this state, engineering or land surveying, as defined in the provisions of this chapter, or to use in connection with his name or otherwise assume, use, or advertise any title or description tending to convey the impression that he is a professional engineer or a land surveyor, unless such a person has been duly registered under the provisions of this chapter.

Texas is the only state that requires, under some conditions, software engineers to be licensed About two years ago there were 50,513 licensed professional engineers in Texas (some inactive) Of those only 60 are primarily in software engineering, about .1% of the total and of those, a fifth are in universities UW CSE P503 David Notkin Autumn 2007 14 Basics of program correctness

In a logic, write down (this is often called the specification) the effect of the computation that the program is required to perform (the postcondition Q) any constraints on the input environment to allow this computation (the precondition P) Associate precise (logical) meaning to each construct in the programming language (this is done per-language, not perprogram) Reason (usually backwards) that the logical conditions are satisfied by the program S A Hoare triple is a predicate {P}S{Q} that is true whenever P holds and the execution of S guarantees that Q holds UW CSE P503 David Notkin Autumn 2007 15 Examples {true} y := x * x;

{y >= 0} {x <> 0} y := x * x; {y > 0} {x > 0} x := x + 1; {x > 1} UW CSE P503 David Notkin Autumn 2007 16 More examples {x = k} if (OnEscalator(x)x < 0) x := -x endif; { ? } {

? } x := 3; { x = 8 } UW CSE P503 David Notkin Autumn 2007 17 Strongest postconditions [example from Aldrich and perhaps from Leino] The following are all valid Hoare triples {x = 5} x := x * 2 { true } {x = 5} x := x * 2 { x > 0 } {x = 5} x := x * 2 { x = 10 || x = 5 } {x = 5} x := x * 2 { x = 10 } Which is the most useful, interesting, valuable? Why?

UW CSE P503 David Notkin Autumn 2007 18 Weakest preconditions [example from Aldrich and perhaps from Leino] Here are a number of valid Hoare Triples {x = 5 && y = 10} z := x / y { z < 1 } {x < y && y > 0} z := x / y { z < 1 } {y 0 && x / y < 1} z := x / y { z < 1 } The last one is the most useful because it allows us to invoke the program in the most general condition It is called the weakest precondition, wp(OnEscalator(x)S,Q) of S with respect to Q If {P} S {Q} and for all P such that {P} P P P, then

P is wp(OnEscalator(x)S,Q) UW CSE P503 David Notkin Autumn 2007 19 Sequential execution What if there are multiple statements {P} S1;S2 {Q} We create an intermediate

assertion {P} S1 {A} S2 {Q} We reason (usually) backwards to prove the Hoare triples A formalization of this approach essential defines the ; operator in most programming languages UW CSE P503 {x > 0} y := x*2; z := y/2 {z > 0} {x > 0} y := x*2; {y > 0} z := y/2 {z > 0}

David Notkin Autumn 2007 20 Conditional execution {P} if C then S1 else S2 endif {Q} Must consider both branches Ex: compute the maximum of two variables x and y UW CSE P503 {true} if x >= y then

max := x else max := y fi {(OnEscalator(x)max >= x max >= y)} David Notkin Autumn 2007 21 Hoare logic rule: conditional {P} if C then S1 else S2 {Q} {P C}S1{Q} {P C}S2{Q} UW CSE P503 David Notkin Autumn 2007 22

Be careful! {true} max := abs(OnEscalator(x)x)+abs(OnEscalator(x)y); {max >= x max >= y} This predicate holds, but we dont want it to The postcondition is written in a way that permits satisfying programs that dont compute the maximum In essence, every specification is satisfied by an infinite number of programs and vice versa The right postcondition is {(OnEscalator(x)max = x max = y) (OnEscalator(x)max >= x max >= y)} UW CSE P503 David Notkin Autumn 2007 23 Out of sorts (example from last time) (OnEscalator(x) i,j i < j a[i] a[j])

A = permutation(OnEscalator(x)A) Its even more complicated if you want to define a stable sorting specification one that leaves equal keys in the same order as they were in the original array UW CSE P503 David Notkin Autumn 2007 24 Assignment statements Weve been highly informal in dealing with assignment statements What does the statement x := E mean? {Q(OnEscalator(x)E)} x := E {Q(OnEscalator(x)x)} If we knew something to be true about E before the assignment, then we know it to be true about x after the assignment (assuming no side-effects)

UW CSE P503 David Notkin Autumn 2007 25 Examples {y > 0} x := y {x > 0} {x > 0} [Q(E) x + 1 > 1 x > 0 ] x := x + 1; {x > 1} [Q(x) x > 1] UW CSE P503 David Notkin Autumn 2007 26

More examples { ? } x := y + 5 {x > 0} {x = A t := x := y := {x = B UW CSE P503 y = B } x; y; t y = A } David Notkin Autumn 2007

27 Loops {P} while B do S {Q} We can try to unroll this into {P B} S {Q} {P B} S {Q B} {P B} S {Q B} S {Q B} But we dont know how far to unroll, since we dont know how many times the loop can execute The most common approach to this is to find a loop invariant, which is a predicate that is true each time the loop head is reached (on entry and after each iteration)

and helps us prove the postcondition of the loop It approximates the fixed point of the loop UW CSE P503 David Notkin Autumn 2007 28 Loop invariant for {P} while B do S {Q} Find I such that P I {B I} S {I} {B I} Q Example -Invariant is correct on entry Invariant is maintained

Loop termination proves Q {n > 0} x := a[1]; i := 2; while i <= n do if a[i] > x then x := a[i]; i := i + 1; end; {x = max(OnEscalator(x)a[1],,a[n]) UW CSE P503 David Notkin Autumn 2007 29 Termination

Proofs with loop invariants do not guarantee that the loop terminates, only that it does produce the proper postcondition if it terminates this is called weak correctness A Hoare triple for which termination has been proven is strongly correct Proofs of termination are usually performed separately from proofs of correctness, and they are usually performed through well-founded sets In this example its easy, since i is bounded by n, and i increases at each iteration Historically, the interest has been in proving that a program does terminate: but many important programs now are intended not to terminate UW CSE P503 David Notkin Autumn 2007

30 What else? Dijkstras weakest precondition (wp) formulation is a more popular alternative to Hoare triples wp(OnEscalator(x)S,Q) is the weakest precondition such that if S is executed, Q will be true {P}S{Q} P wp(OnEscalator(x)S,Q) Need logic rules for procedure calls (with different parameter passing mechanisms), pointers, gotos, concurrency, dynamic dispatch, UW CSE P503 David Notkin Autumn 2007 31 Correctness of data structures Primarily due to Hoare;

figures from Wulf et al. < x ,x > Prove the specifications on the abstract operations (e.g., R Pusha) Prove the specifications on S .s p = 2 the concrete operations S .v = (e.g., Pushc) [x x ,? ,? ,...] Prove the relation between abstract and concrete operations (e.g., R), the representation mapping {full(OnEscalator(x)Sa)} 1 P u s h a (S ,x ) < x ,x 1 ,x 2 >

2 R P u s h c(S ,x ) 2, 1 Pusha(OnEscalator(x)Sa,x) {Sa=||Sa} UW CSE P503 David Notkin Autumn 2007 S .s p = 3 S .v = [x 2 ,x 1 ,x ,? ,...] Example

{full(OnEscalator(x)R(OnEscalator(x)Sc))} Pushc(OnEscalator(x)Sc,x) {R(OnEscalator(x)Sc) = || R(OnEscalator(x)Sc)} 32 So what? I just spent time showing you stuff that I said isnt especially useful Its tedious and error-prone If we cant get our programs right, why should we believe we get our detailed proofs right? One answer: tools, such as proof assistants Its hard with real programming languages and programs But it does lay a foundation for Thinking about programs more precisely Applying techniques like these in limited, critical situations

Development of some modern specification and analysis approaches that seem to have value in more situations UW CSE P503 David Notkin Autumn 2007 33 Interlude: an empirical result (story) Reliability in hardware is often improved by replicating components N-version programming was an attempt by Avizienis and colleagues to improve software reliability in a similar way In particular, the idea was to have independently produced software act as replicated components with the expectation that there would be a low probability of identical software faults occurring in different versions

UW CSE P503 David Notkin Autumn 2007 34 Knight and Leveson experiment Knight & Leveson evaluated the assumption of independence in N-version programming through a careful experiment They found that the assumption of independence of failures failed statistically UW CSE P503 David Notkin Autumn 2007 35 Another empirical result: Votta Does every inspection need a meeting?

At each step in large software development, reviewers carry out inspections to detect faults. These inspections are usually followed by a meeting to collect the faults that have been discovered. However, we have found that these inspection meetings are not as beneficial as managers and developers think they are. Even worse, they cost much more in terms of products development interval and developer's time than anyone realizes. Analysis of the inspection and collection process leads us to make the following suggestions. First, at the least, the number of participants required at each inspection meeting should be minimized. Second, we propose ... UW CSE P503 David Notkin Autumn 2007 36 Formal methods

The failure of proof of correctness to meet its promises caused a heavy decrease in interest in the late 1970s and the 1980s There has been a resurgence of interest in formal methods starting in the late 1980s and through the 1990s Mostly due to potential usefulness in specification and a few success stories Still not entirely compelling to me, in a broad sense, but definitely showing more promise Key issues to me include Partial specifications (proving little theorems about big programs instead of big theorems about little programs B. Scherlis) and incremental benefit Tool support (making specifications electric D. Jackson) and automated analysis What domains, and applied by whom? UW CSE P503

David Notkin Autumn 2007 37 Potential benefits Increased clarity Ability to check for internal consistency This is very different from program correctness, where the issue was to show that a program satisfied a specification Ability to prove properties about the specification Related to M. Jacksons refutable descriptions Provides basis for falsification (a fancy word for debugging) Perhaps more useful than verification UW CSE P503 David Notkin Autumn 2007 38

C.A.R. Hoare, 1988 Of course, there is no fool-proof methodology or magic formula that will ensure a good, efficient, or even feasible design. For that, the designer needs experience, insight, flair, judgement, invention. Formal methods can only stimulate, guide, and discipline our human inspiration, clarify design alternatives, assist in exploring their consequences, formalize and communicate design decisions, and help to ensure that they are correctly carried out. UW CSE P503 David Notkin Autumn 2007 39 Observation From a specification of a small telephone system a subscriber is a sequence of digits. Let Subs be the set of all

subscribers ...certain digit sequences correspond to unobtainable numbers, and some are neither subscribers, nor are they unobtainable. Only a mathematician could treat the real world with such audacious disdain. M. Jackson UW CSE P503 David Notkin Autumn 2007 40 Anthony Halls view VS. And Martyn Thomas sez

UW CSE P503 David Notkin Autumn 2007 41 Model-oriented Model a system by describing its state together with operations over that state An operation is a function that maps a value of the state together with values of parameters to the operation onto a new state value A model-oriented language typically describes mathematical objects (e.g. data structures or functions) that are structurally similar to the required computer software UW CSE P503 David Notkin Autumn 2007

42 Z (zed) Perhaps the most widely known and used modelbased specification language Good for describing state-based abstract descriptions roughly in the abstract data type style Real ADT-oriented specifications are generally does as algebraic specifications Based on typed set theory and predicate logic A few commercial successes Ill come back to one reengineering story afterwards UW CSE P503 David Notkin Autumn 2007 43 Basics Static schemas

States a system can occupy Invariants that must be maintained in every system state Dynamic schemas Operations that are permitted Relationship between inputs and outputs of those operations Changes of states UW CSE P503 David Notkin Autumn 2007 44 The classic example A birthday book that tracks peoples birthdays and can issue reminders of those birthdays There are tons of web-based versions of these now There are two basic types of atomic elements in this

example [NAME,DATE] An inherent degree of abstraction: nothing about formats, possible values, etc. UW CSE P503 David Notkin Autumn 2007 45 Off to the whiteboard for the classic Z BirthdayBook example UW CSE P503 David Notkin Autumn 2007 46 Points about Z

This isnt proving correctness between a specification and a program There isnt a program! Even the specification without the implementation has value The most obvious example is when a theorem is posited and then is proven from the rest of the specification known = known {name?}name?} The actual notation seems more effective that some others The Z is intended to be in bite-sized chucks (schema), interspersed with natural language explanations UW CSE P503

David Notkin Autumn 2007 47 Schema calculus: sweet! The schema calculus allows us to combine specifications using logical operators (e.g., , , , ) This allows us to define the common and error cases separately, for example, and then just -ing them together In some sense, it allows us to get a cleaner, smaller specification UW CSE P503 David Notkin Autumn 2007 48 But dont try this on programs!

Wouldnt it be fantastic if we had the equivalent of the schema calculus on programs? Write your error cases separately and then just them together Write a text editor and a spell checker and integrate them by -ing them together So you want to build a program that doesnt blow up a nuclear power plant? Just build one that does, and then negate it ! Programs are not logic Some classes of programming languages largely functional languages come closer than imperative and OO languages UW CSE P503 David Notkin Autumn 2007

49 Z used to improve CICS/ESA_V3.1 A broadly used IBM transaction processing system Integrated into IBM's existing and well-established development process Many measurements of the process indicated that they were able to reduce their costs for the development by almost five and a half million dollars Early results from customers also indicated significantly fewer problems, and those that have been detected are less severe than would be expected otherwise UW CSE P503 David Notkin Autumn 2007 50

1992 Queens Award for Technological Achievement Her Majesty the Queen has been graciously pleased to approve the Prime Minister's recommendation that The Queen's Award for Technological Achievement should be conferred this year upon Oxford University Computing Laboratory. Oxford University Computing Laboratory gains the Award jointly with IBM United Kingdom Laboratories Limited for the development of a programming method based on elementary set theory and logic known as the Z notation, and its application in the IBM Customer Information Control System (CICS) product. UW CSE P503 David Notkin Autumn 2007 51 ...

The use of Z reduced development costs significantly and improved reliability and quality. Precision is achieved by basing the notation on mathematics, abstraction through data refinement, re-use through modularity and accuracy through the techniques of proof and derivation. CICS is used worldwide by banks, insurance companies, finance houses and airlines etc. who rely on the integrity of the system for their day-to-day business. UW CSE P503 David Notkin Autumn 2007 52 Other success stories

There are a few other success stories, too (not all Z!) Ex: Garlan and Delisle. "Formal Specification of an Architecture for a Family of Instrumentation Systems" (1995) Aided Tektronix in unifying their understanding and development processes for a broad range of oscilloscopes, function generators, etc. Clarke and Wing. Formal methods: state of the art and future directions. ACM Computing Surveys 28(4), 1996. Craigen, Gerhart, Ralston. An International Survey of Industrial Applications of Formal Methods, Volumes I & II (Purpose, Approach, Analysis and Conclusions; Case Studies), NIST, 1993. UW CSE P503 David Notkin Autumn 2007 53

Tool support for Z? Some commercial, some freeware Formatting (handling all those characters) html extensions ZML Type checkers Proof editors, proof assistants, provers Specification animations UW CSE P503 David Notkin Autumn 2007 54 Analyzing specifications

It is easy to write specifications that are inconsistent Daniel Jackson and colleagues have developed a sequence of tools that check Z-like specifications for inconsistencies You feed a specification to the tool and it says either Heres a problem, and heres a specific (counter)example of it, or I cant find one (although there may be one) Examples include paragraph style mechanisms, telephone switch structures, many more (generally relatively small) Pieces of the ideas appear in Jackson and Chapin. Redesigning Air-Traffic Control: A Case Study in Software Design. IEEE Software, May/June 2000 His Alloy system is the most recent of these tools well play with it some for an assignment (most likely) UW CSE P503

David Notkin Autumn 2007 55 An example (skipping lots of steps): Jackson & Vaziri class List {List next; Val val;} void static delete (OnEscalator(x)List l, Val v) { List prev = null; while (OnEscalator(x)l != NULL) if (OnEscalator(x)l.val == v) { prev.next = l.next ; Procedure for deleting all return; } elements with a given value else { from a singly linked list prev = l ; Relational formulae are l = l.next ;

automatically extracted } Fields of List treated as binary relations next: List List val: List Val UW CSE P503 David Notkin Autumn 2007 56 Desired properties of delete 1. 2. 3. 4. 5.

Running the tool shows that Properties 1, 4 and 5 No cells are added appear to hold l.*next in l.*next But not properties 2 and 3 No cell with value v afterwards Property 2 fails because no c:l.*next|c.val=v the first list cell cannot be deleted All cells with value v removed l.*next = l.*next-{c|c.val=v} Even a simple fix shows another error, in which No cells mutated the last two cells share all c|c.val = c.val a value equal to v No cycles introduced no c:l.*next|c in c.+next ->

no c:l.*next|c in c.+next UW CSE P503 David Notkin Autumn 2007 57 Underlying technologies The Jackson et al. tools have been based on (primarily) two different technologies Model checking: explicit state space enumeration, BDDbased symbolic model checking Constraint satisfaction (boolean satisfiability): stochastic (WalkSAT), deterministic (Davis-Putnam, SATO, RelSAT) They generally use some form of bounded checking based on the small scope hypothesis, which argues that a high proportion of bugs can be found by testing the program for all

test inputs within some small scope. If the hypothesis holds, it follows that it is more effective to do systematic testing within a small scope than to generate fewer test inputs of a larger scope. [Andoni et al.] UW CSE P503 David Notkin Autumn 2007 58 Interlude: mylyn from tasktop.com Note: co-developed and co-founded by my former student, Gail Murphy Mylyn is the Task-Focused UI for Eclipse that reduces information overload and makes multi-tasking easy. It does this by making tasks a first class part of Eclipse, and integrating rich and offline editing for repositories such as Bugzilla, Trac, and

JIRA. Once your tasks are integrated, Mylyn monitors your work activity to identify information relevant to the task-at-hand, and uses this task context to focus the Eclipse UI on the interesting information, hide the uninteresting, and automatically find what's related. This puts the information you need to get work done at your fingertips and improves productivity by reducing searching, scrolling, and navigation. UW CSE P503 David Notkin Autumn 2007 59 Finite state machines There is a large class of specification languages based on finite state machines A finite set of states A finite alphabet of symbols A start state and zero or more final states A transition relation

Often used for describing the control aspects of reactive systems (and much, much more!) The theoretical basis is very firm UW CSE P503 David Notkin Autumn 2007 60 Many, many models Petri nets Communicating finite state machines Statecharts RSML

UW CSE P503 David Notkin Autumn 2007 61 Walkman example (due to Alistair Kilgour, Heriot-Watt University) UW CSE P503 David Notkin Autumn 2007 62 A common problem It is often the case that conventional finite state machines blowup in size for big problems, in two senses The actual description of the machine can get very large The state space represented by the machine can get to be

enormous This is especially true for deterministic machines (which are usually desirable) and machines capturing concurrency (because of the potential interleavings that must be captured) UW CSE P503 David Notkin Autumn 2007 63 Statecharts (Harel) A visual formalism for defining finite state machines A hierarchical mechanism allows for complex machines to be defined by smaller descriptions Parallel states (AND decomposition) Conventional OR decomposition Now part of UML UW CSE P503

David Notkin Autumn 2007 64 Tools Statecharts have a set of supporting tools from iLogix (STATEMATE, Rhapsody) Editors Simulators Code generators C, Ada, Verilog, VHDL Some analysis support UML tools and environments UW CSE P503 David Notkin Autumn 2007 66 i-Logix screenshot (old)

UW CSE P503 David Notkin Autumn 2007 67 Analysis Given a Statecharts description, how can one tell if it has some desirable properties? For instance, is it deterministic? Are there deadlocks? And domain-specific properties, too The most promising technology for helping with this is model checking, which well look at next week Model checking has also moved into applications to code as well as specifications UW CSE P503 David Notkin Autumn 2007

68

Recently Viewed Presentations

  • Todays webinar: Social enterprise 14 May 2019 Acknowledgement

    Todays webinar: Social enterprise 14 May 2019 Acknowledgement

    Various organisations in Australia representing SESocial Ventures Australiaworks with partners to alleviate disadvantage Social Traders connecting social enterprises with social procurement opportunities and supporting social enterprise to successfully deliver on the contracts they win, jointly funded by the Dara Foundation...
  • Proof by resolution - cs.ubc.ca

    Proof by resolution - cs.ubc.ca

    Slide credit: some slides adapted from Stuart Russell (Berkeley), some from Prof. Carla P. Gomes (Cornell) Lecture 21. Some slides Prof. Carla P. Gomes. [email protected] CPSC 422, Lecture 21. Slide . David Buchman and Professor David Poole are the recipients...
  • Assessing Writing - Mrs. Potts Class

    Assessing Writing - Mrs. Potts Class

    Graphophonic. Pragmatic. Similar Goals/Skills of Reading and Writing(Pinnell, 1999) ... Examples of Writing Stages(Stages 5 through 7) Instructional Practices for Bilingual Students. Provide extended periods of time for students to write, and allow personal choice of topic and genre. ...
  • Advanced Algorithm Design and Analysis (Lecture 1)

    Advanced Algorithm Design and Analysis (Lecture 1)

    Advanced Algorithm Design and Analysis (Lecture 3) SW5 fall 2004 Simonas Šaltenis E1-215b [email protected] Text-search Algorithms Goals of the lecture: Naive text-search algorithm and its analysis; Rabin-Karp algorithm and its analysis; Knuth-Morris-Pratt algorithm ideas; Boyer-Moore-Horspool algorithm and its analysis.
  • Assessment and Reporting - WordPress.com

    Assessment and Reporting - WordPress.com

    Assessment and Reporting. EDFGC 5807 Theory and Practice of Learning and Teaching. Week 9. Monday 8thMay 2017
  • The Impact Of Communication Technology & The Media

    The Impact Of Communication Technology & The Media

    The media helps us to learn more about the world around us It shows us how people in other parts of the world live. Closer Together We feel closer to each other as a country (collective identity) when we cheer...
  • Shenghui Wang Vrije Universiteit Amsterdam swang@few.vu.nl Practical device?

    Shenghui Wang Vrije Universiteit Amsterdam [email protected] Practical device?

    Still attached to existing databases and categorised through Western KR Using indigenous conceptualisations to Organise exhibitions Construct e-learning materials Decolonise information access to the collections 4. Building intercultural bridges A spiral model for building intercultural bridges What to check?
  • Future Wireless Network Architecture Driven by Broadband Data

    Future Wireless Network Architecture Driven by Broadband Data

    In my view, the only way to -- and failing to deliver on any one of these prongs will leave us where we started - is this: We need a lot of spectrum A next generation OFDM based technology An...