text:
Specication and Renement with
- Daniela Montgomery
- 3 years ago
- Views:
1 Chapter 6 On the Verication of VDM Specication and Renement with PVS Sten Agerholm, Juan Bicarregui and Savi Maharaj Summary This chapter describes using the PVS system as a tool to support VDM- SL. It is possible to translate from VDM-SL into the PVS specication language in a very easy and direct manner, thus enabling the use of PVS for typechecking and verifying properties of VDM-SL specications and renements. The translation is described in detail and illustrated with examples. The drawbacks of the translation are that it must be done manually (though automation may be possible), and that the \shallow embedding" technique which is used does not accurately capture the proof rules of VDM-SL. The benets come from the facts that the portion of VDM-SL which can be represented is substantial and that it is a great advantage to be able to use the powerful PVS proof-checker. A variety of examples of verications using PVS are described in the chapter. 6.1 Introduction The PVS system[13], developed at SRI Menlo Park, in California, combines an expressive specication language with a powerful theorem-proving tool in which interactive proof is tightly integrated with many automatic procedures which speed up routine parts of proof development. The combination makes for a user-friendly system which is easy to learn and to use for doing non-trivial theorem-proving. The specication language is based on classical higher-order logic, enriched with a type
2 158 CHAPTER 6. VDM PROOFS IN PVS system based on Church's simple theory of types with extensions for subtyping and dependent types. The result is an expressive language which has much in common with formal notations such as VDM-SL. A system of parameterized theories provides structuring for developments and extensive libraries add denitions of many useful mathematical constructs similar to those used in VDM-SL. The striking, if supercial, similarity between VDM-SL and the PVS specication language means that a signicant portion of VDM-SL may be represented very directly in PVS. This gives rise to an informal \shallow embedding" [10] of a substantial portion of VDM-SL. The embedding makes use of the parameterized theories of PVS to represent VDM-SL specications and renement relationships between pairs of specications. The result is a simple and direct means of harnessing the power of the PVS proof-checker for proving validation conditions and proof obligations arising from specications and renements. The embedding also provides automatic generation of some proof obligations which can be made to arise as type-checking constraints (TCCs) in PVS. The drawbacks of the method are that translation must (at present) be performed manually, and that the proof rules of VDM-SL are not accurately captured because of dierences between the logics of VDM-SL and PVS. The latter fact implies that what we are doing would be more accurately described as VDM-style specication. Using this approach outlined above, we have hand-translated a number of VDM- SL specications and renements into the PVS logic, and used the prover to check various properties of these specications. This process resulted in the detection of several errors in some of these specications. In this chapter we describe one medium-sized example which illustrates most of the aspects of our approach. The structure of the chapter is as follows. In Section 6.2 we briey describe the PVS system. This is followed in Section 6.3 by an informal presentation of the translation from VDM-SL to the PVS specication language. Section 6.4 complements Section 6.3 by illustrating through the use of an example how a specication as a whole is represented as a PVS theory. In this section we also discuss using the PVS proof-checker to typecheck the example specication and to prove various validation conditions about it. In Section 6.5 we turn to the subject of renement, showing how the example of Section 6.4 can be represented in PVS as a renement ofa more abstract specication, and how the PVS proof-checker was used to discharge all the resulting proof obligations. In the nal sections we discuss the validity of our informal translation from VDM-SL to PVS, make some observations about what was learned during this exercise, and present our conclusions. 6.2 The PVS System The PVS system is produced by a team of researchers at SRI International, in California. The philosophy behind the system is that it should provide a high degree of support for requirements specication, since errors at this initial stage are considered to be the most costly. However, the system itself is general purpose and
3 6.3. FROM VDM-SL TO THE HIGHER ORDER LOGIC OF PVS 159 lends itself to a variety of applications [13], including verications of algorithms and hardware systems and embeddings of other logics. The foundation of the system is the expressive PVS Specication Language. This is based on classical higher-order logic, enhanced with a rich system of types including subtyping, dependent types and recursive types. Specications may be structured using a system of parameterized theories. Various aspects of the syntax of the PVS specication language will be explained where they arise in the chapter. The PVS specication language is supported by a collection of tools including a type checker and an interactive proof checker. The tools run under emacs which provides a basic user interface. Typechecking in PVS is undecidable and generally results in the generation of proof obligations called type-checking constraints (TCCs). TCCs may be proved by invoking a powerful tactic called tcp or, if this tactic fails, by use of the PVS proof-checker. One of the main attractions of the PVS proof-checker is that basic proof commands are tightly integrated with powerful decision procedures and tactics. The tactics may be combined in various ways to form proof strategies. Some of the most commonly used tactics embody simple proof rules (splitting conjunctions and disjunctions, instantiating quantiers, skolemizing, etc). Others implement sophisticated decision procedures. Examples are the tactic PROP for propositional simplication and the all-powerful tactic GRIND, which subsumes PROP and does much more. Other tactics such as HIDE allow management of the proof state. The version of PVS referred to in this chapter is the \alpha-plus" release available in June From VDM-SL to the Higher Order Logic of PVS A large subset of VDM-SL can be translated into a higher order logic such as the PVS specication language. This section describes such a translation in sucient detail to support manual translations, though more formality might be required in order to support an implementation of the translation process. The translation method may beviewed as a (very) shallow embedding of VDM-SL in PVS. The syntax of VDM-SL constructs is not embedded: we work with the \semantics" of the constructs directly. Therefore it can be argued that the translation is not safe (in a logical sense). This is a disadvantageofshallowembeddings in general, though some shallow embeddings are more safe than others. The translation of VDM-SL to PVS is relatively safe in this sense since PVS and VDM-SL share many concepts and constructs. One of the dierences between VDM-SL and PVS is that a VDM-SL expression can be undened there is one common undened element toalltypes, which can be viewed as sets. For example, an expression is undened if a divisor is zero, if a nite sequence is applied to an index outside its indices, or if a pattern match in
4 160 CHAPTER 6. VDM PROOFS IN PVS a let expression fails. Most of such situations are handled implicitly by restrictions on the translation of various constructs, in combination with type checking in PVS. For instance, PVS itself generates type checking conditions to capture division by zero. A related factor is that PVS does not support partial functions. All VDM-SL functions are translated to PVS functions and PVS generates an obligation stating that a given function must be total. Partial functions are discussed in more depth in Section 6.6. Belowwe discuss how various constructs of VDM-SL specications can be translated. We show VDM-SL expressions in the ASCII notation supported by the IFAD VDM- SL Toolbox Basic Types, the Product Type and Type Invariants Boolean and number types can be viewed as sets and translated directly to the corresponding types in PVS. It is not necessary to edit arithmetic expressions and logical connectives since they have the same symbols and names in PVS. Specially, the connectives and and or are used as \and-also" and \or-else" in both the Toolbox version of VDM-SL and PVS. Hence, it is allowed to write \P(x) and x/x = 1" if one can prove the automatically generated condition \P(x) IMPLIES x /= 0". Restricted quantications are translated to quantications over PVS subtypes. Hence, a universal quantication like forall x in set s & P[x] can be translated to forall (x:(s)): P[x]. Note that the & is replaced with : and we insert brackets around the binding. In VDM-SL it is possible to specify a subtypeofatype by writing a predicate that the elements of the subtype must always satisfy. This predicate is called an invariant. As an example consider the denition of a type of positive reals: Realp = real inv r == r >= 0 This introduces a new constant inv_realp implicitly, which equals the invariant predicate. The denition is translated to PVS as follows: inv_realp(r:real) : bool = r >= 0 Realp: TYPE = (inv_realp) The type Realp is dened as a subtype of the built-in type real. The product type of VDM-SL can be translated directly to the product type of PVS. VDM-SL tuples are written using a constant mk_, e.g. mk_(1,2,3). This constant could be ignored in the translation, but instead we have introduced and usually use a dummy constant mk_, dened as the identity function. The only way to split a tuple in VDM-SL is using pattern matching on mk_, e.g. in a let expression like let mk_(x,y,z) = t in e. The translation of pattern matching is discussed in more detail in Section
5 6.3. FROM VDM-SL TO THE HIGHER ORDER LOGIC OF PVS Record Types VDM-SL records are translated directly to records in PVS. There is only a slight dierence in syntax. PVS does not automatically introduce a constructor function mk_a as in VDM-SL for a record denition called A, but the function is easy to dene. Below, we rst give an example of how to translate a standard record type denition and then give a more complicated example where an invariant is also specied. Standard Records We consider a simple example, which denes a record of points in the two-dimensional positive real plane. The VDM-SL denition of the record type is (Realp was introduced above): Point:: x: Realp y: Realp This is translated to PVS as follows: Point: TYPE = [# x: Realp, y: Realp #] In both cases, eld selectors x and y are introduced implicitly. Unfortunately, PVS does not support the VDM-SL notation for eld selection, which is the standard one using a dot and the eld name, e.g. p.x for some point p. Instead elds are viewed as functions that can be applied to records. Thus the VDM-SL expression p.x translates to the PVS expression x(p). The PVS notation is less convenient, e.g. a nested eld selection as in r.a.b.c translates to c(b(a(r))). In VDM-SL each new record denition generates a new \make" function for building elements of the record. In order to allow a direct translation of such expressions to the same expressions in PVS, the constructor function is dened along with a record denition. The constructor for points is: mk_point(a:realp,b:realp) : Point = (# x:= a, y:= b #) In VDM-SL such make constructors are also used for pattern matching in function denitions and in let expressions but this is not possible in PVS. Instead we use Hilbert's choice operator (choose), as described in Section VDM-SL also provides an is_ test function for records, which is sometimes used to test where elements of union types come from. Since we do not support union types properly (see Section 6.3.4) we shall ignore this constant. Records with Invariants Sometimes a VDM-SL record denition is written with an invariant. For instance, an equivalent way of dening the point record above would be the following denition
6 162 CHAPTER 6. VDM PROOFS IN PVS Point:: x: real y: real inv mk_point(x,y) == x >= 0 and y >= 0 where an invariant is used to specify that we are only interested in the positive part of the two-dimensional real plane. We translate this as follows: inv_point(x:real,y:real) : bool = x >= 0 and y >= 0 Point: TYPE = {p: [# x:real, y:real #] inv_point(x(p),y(p))} mk_point(z:(inv_point)) : Point = (# x:= x(z), y:= y(z) #) Note that we restrict the arguments of mk_point. For instance, the following denition does not work mk_point(a:real,b:real) : Point = (# x:= a, y:= b #) since we cannot prove that this yields a point for all valid arguments. There is one small semantic dierence between VDM-SL records and the above representation in PVS. In VDM-SL it is allowed to write mk_point(1,-1) though this will not havetype Point. The only use of such a (kind of) junk term would be in inv_point(mk_point(1,-1)), which would equal false. In the PVS representation, this invariant expression is written as inv_point(1,-1) Sequences, Sets and Maps In this section, we briey consider the translation of nite sequences, nite sets and nite maps. Invariants on these types are treated much like in the previous section on records. Finite Sets Atype of nite sets is provided in the PVS finite_sets library. Thetype is dened as a subtype of the set type, which represents sets as predicates. Most operations on sets exist, or can be dened easily. Oneannoying factor is that for instance set membership, set union and set intersection are all prex operations in PVS. E.g. one must write member(x,s) for the VDM-SL expression \x in set s". Moreover, user-dened constants must be prex and one cannot dene new symbols. PVS supports only a simple and restricted syntax of expressions. Finite Sequences VDM-SL nite sequences can be represented as nite sequences or as nite lists in PVS. The dierence is that nite sequences are represented as functions and nite
7 6.3. FROM VDM-SL TO THE HIGHER ORDER LOGIC OF PVS 163 lists as an abstract datatype. There is more support for nite lists, so we have usually chosen this type as the representation. An advantage of sequences is that indexing is just function application. However, with both representations one must be careful since indexing of sequences starts from one in VDM-SL and from zero in PVS. The safest thing to do is therefore to dene new indexing operations in PVS and use these for the translation. Finite Maps PVS does not support nite maps, so an appropriate theory must be derived from scratch. In doing this, one could probably benet from the paper on nite maps in HOL by Collins and Syme [12], who have implemented their work in a HOL library. However, many operations on nite maps are not supported in this library, so an extended theory of nite maps must be worked out. As a start one could just axiomatize maps in PVS, e.g. by introducing maps as an uninterpreted subtype of the function type, with a few appropriate denitions (and axioms). In fact, for the examples very little support was needed. A representation of maps using functions has advantages. Map application will just be function application and map modication can be translated to PVS with expressions. For example, the VDM-SL map modication m ++f 1 -> 2, 2 -> 3 g, where a map m from numbers to numbers is modied to send 1 to 2 and 2 to 3, translates to m with [ 1 -> 2, 2 -> 3 ] Union Types In VDM-SL, the union of two or moretypes corresponds to the set union of the types. Thus, the union type is a non-disjoint union, if two types have a common element this will be just one element in the union type. Higher order logics do not support non-disjoint unions, but support disjoint sums (unions) or abstract datatypes as in PVS. In general, a VDM-SL union type cannot be translated easily to a PVS datatype. However, if the component types of the union are disjoint then this is partly possible. The translation is only satisfactory when the component types are quote types these correspond to singleton sets. Union of Disjoint Types The union of disjoint types can be represented as a new datatype with constructor names for the dierent types. This representation is not perfect, the component types does not become subtypes of the union type as in VDM-SL. For example this means that the operators dened on the individual types are not inherited as in VDM-SL, where the dynamic type checking ensures that arguments of operators have the right types. In the special case where all components of the union type are new types, it might be possible to dene the union type rst and then dene each
8 164 CHAPTER 6. VDM PROOFS IN PVS of the component type as subtypes of this. Such tricks would not be easy to employ in an automatic translation. Enumerated Types An enumerated type is a union of quote types, which is written using the following ASCII syntax in VDM-SL: ABC = <A> <B> <C>. This can be translated almost directly to PVS, with some minor syntax changes: ABC: TYPE = {A,B,C}. PVS does not support identiers enclosed in < and > Function Denitions Total functions are translated directly to PVS functions. As mentioned before, partial functions cannot be translated in this way. Aswe shall see in Section 6.6, it is possible to encode some partial functions as total functions in PVS by using subtypes to represent their domains of denition. Other formalizations are also possible (see e.g. [2, 1]). Polymorphic functions are not considered at the moment. Standard explicit function denitions, which are function denitions that do not have postconditions, can be translated directly to PVS, if they are not recursive. A precondition will be translated to a subtype predicate. If functions are recursive we must demonstrate that they are total functions in PVS. It is up to the translator to specify an appropriate measure, which is decreased in each recursive call, for the termination proof. Moreover, VDM-SL supports mutual recursive function denitions which would not be easy to translate. The example specications used only few recursive denitions and these were very simple. Implicit function denitions, which are specied using pre- and postconditions only and have no function body, can be represented using the choice operator. Almost equivalently, one can also use function specication, which is a way of dening partially specied functions it is only specied on a subset of a type how a function behaves, and this is specied by an \underdetermined" relation, not an equation [18, 15]. Implicit Denition Let us rst consider the following semi-abstract example of an implicit function denition in VDM-SL: f(x:real,y:real) z:point pre p[x,y] post q[x,y,z] where the variables in square brackets may occur free in the precondition p and the postcondition q. This translates to the following PVS denitions: pre_f(x:real,y:real) : bool = p[x,y]
9 6.3. FROM VDM-SL TO THE HIGHER ORDER LOGIC OF PVS 165 post_f(t:(pre_f))(z:point) : bool = let (x,y) = t in q[x,y,z] f: FUNCTION[t:(pre_f) -> (post_f(t))] The precondition is translated to a predicate on the arguments of the function and the postcondition is translated to a binary relation on the arguments and the result. The function itself is dened as an uninterpreted constant using a dependent function type: given arguments t satisfying the precondition it returns a result satisfying the postcondition, or more precisely, a result related to t by the postcondition. This relation may be underdetermined, i.e. it may specify a range of possible values for a given input, but the function will always return a xed value in this range. If the precondition is not satised the result is an arbitrary value. As a result of an uninterpreted constant denition, the PVS type checker generates an existence condition, which says that we must prove there exists a value in the specied type. Hence, above we must prove there exists a function from the precondition to the postcondition. In general, proving this condition can be non-trivial, since one must usually provide a witness, i.e. a function of the specied form. (For instance, it would be dicult to prove that there exists a square root function.) Explicit Denition Explicit denitions of recursive functions can be problematic for automatic translation since a translator must insert a well-founded measure for proofs of termination. This is easy enough when the recursion is simple, which it is for primitive recursive functions over numbers and abstract datatypes, but for more general recursive functions this can be hard. PVS has some strategies for proving termination in simple cases. An explicit function denition has no postcondition but instead a direct denition, and perhaps a precondition. Let us consider a standard example of a primitive recursive function on the natural numbers: fac: nat -> nat fac(n) == if n = 0 then 1 else n * fac(n-1) pre 0<=n This translates to the following PVS denitions: pre_fac(n:nat) : bool = n >= 0 fac(n:(pre_fac)) : recursive nat = if n = 0 then 1 else n * fac(n-1) endif measure (lambda (n:(pre_fac)): n) Note that we have inserted \recursive" and\measure", which are part of the syntax for recursive function denitions in PVS. The measure is used to generate
10 166 CHAPTER 6. VDM PROOFS IN PVS conditions for termination of recursive calls. (The precondition is redundant above, it is included for illustration.) Pattern Matching Pattern matching plays an important role in VDM-SL specications. It is used frequently to get access to the values at elds of a record, and it is the only way to get access to the values of the components of a tuple. We can represent a successful pattern matching but not a failing one, since we do not represent undened expressions. However, undened expressions are either avoided due to type checking, or else represented by arbitrary values, i.e. values of a certain type that we donotknow anything about. Pattern Matching in Let Expressions Here are some examples which use a record type A with three elds a, b and c. Assuming x, y and z are variables, the following VDM-SL let expression let mk_(x,y,z) = e1 in e2[x,y,z] can be translated to exactly the same term in PVS, except that the tuple constructor mk_ must be omitted for the expression to parse. The following VDM-SL let expression with a pattern match on the record type A let mk_a(x,y,z) = e1 in e2[x,y,z] can be translated to the following PVS term: let x = a(e1), y = b(e1), z = c(e1) in e2[x,y,z] The eld selector functions are used to destruct the expression. This corresponds to the way that PVS itself represents pattern matching on tuples (using project functions). If one of the variables in the VDM-SL expression was the don't care pattern, written as an minus sign -, thenwe could just replace this with a new variable. We do not allow constants in patterns in let expressions, since they do not make much sense (they are however allowed in VDM-SL). The following VDM-SL \let-be-such-that" expression let mk_a(x,y,z) in set s be st b[x,y,z] in e[x,y,z] can be translated to let v = (choose ({w:(s) let x = a(w), y = b(w), z = c(w) in b[x,y,z]}) in let x = a(v), y = b(v), z = c(v) in e[x,y,z]
11 6.3. FROM VDM-SL TO THE HIGHER ORDER LOGIC OF PVS 167 where we use the choice operator, choose, to represent the looseness in the VDM-SL specication. Don't care patterns are translated as suggested above, by introducing new variables. We allow constants and other values in let-be-st expressions. For instance, we can translate let mk_a(x,y,0) in set s be st b[x,y] in e[x,y] into the PVS term let v = (choose ({w:(s) let x = a(w), y = b(w), n = c(w) in n = 0 and b[x,y]}) in let x = a(v), y = b(v) in e[x,y] where we include a test in the body of the choose. Pattern Matching in Cases Expressions The following VDM-SL cases expression cases e: mk_a(0,-,z) -> e1, mk_a(x,1,z) -> e2, others -> e3 end can be translated to the following conditional expression in PVS: cond a(e) = 0 -> let z = c(e) in e1, b(e) = 1 -> let x = a(e), z = c(e) in e2, else -> e3 endcond PVS's built-in cases expression only works on abstract datatypes. Pattern Matching in Function Denitions Pattern matching can be used on arguments in a function denition, where the patterns are typically variables (or don't care patterns which are translated to new variables). We can treat this by inventing a new variable using the function denition and then extending the body with a let expression to represent the pattern match. This approach is also used in the formal semantics of VDM-SL.
12 168 CHAPTER 6. VDM PROOFS IN PVS State and Operations A VDM-SL specication may contain a state denition, which species a number of variable names for elements of the state space. The state space is known to operations and nowhere else. The state denition is essentially a record denition and is therefore represented as a record type in PVS. Operations are represented as state transformations, i.e. functions which, in addition to the operation's input values, take the initial state as an argument and return the output state as a result (and possibly an explicit result value). Hence, operation denitions can be translated in a similar way as functions. The body of operation denitions may contain assignments and sequential compositions. Assignments are translated to PVS with expressions and sequential compositions are represented using let expressions. In this chapter we do not consider conditions (which should be easy) and while loops (which probably could be translated to recursive functions). More exotic features such as exception handling are also excluded from consideration. Assume we have the following state denition in VDM-SL: state ST of x: real y: real z: real end This can be translated to: ST: TYPE = [# x: real, y: real, z: real #] mk_st(x:real,y:real,z:real): ST = (# x:=x, y:=y, z:=z #) Now assume we have the sequence: x:=5 y:=3 z:=1 This can be translated to lambda (s:st): let s1 = s with [x:=5], s2 = s1 with [y:=3], s3 = s2 with [z:=1] in s3 or simply to lambda (s:st): s with [x:=5, y:=3, z:=1] since the assignments are independent in this example.
13 6.4. A SPECIFICATION EXAMPLE: MSMIE A Specication Example: MSMIE The Multiprocessor Shared-Memory Information Exchange (MSMIE) is a protocol for \inter-processor communications in distributed, microprocessor-based nuclear safety systems" [17], which has been used in the embedded software of Westinghouse nuclear systems designs. The protocol uses multiple buering to ensure that no \data-tearing" occurs as separate processors communicate via some shared memory. In other words, data should never be overwritten by one process while it is still being read by another. One important requirement is that neither writing nor reading processes should have to wait for a buer to become available another is that recent information should be passed, via the buers, from writers to readers. The example has previously been analyzed using CCS in [11] and using VDM and B in [9]. In common with these analyses, we shall be working with a simplied system in which it is assumed that information is being passed from a single \slave" processor to several \master" processors. Thus, there are several reading processors, \masters", but only one writing, \slave" process. The information exchange is realised by a system with three buers. At any time, one buer is available for writing, one for reading, and the third is either between a write and a read and hence contains the most recently written information, or between a read and a write and so is idle. The status of each buer is recorded by a ag which can take one of four values: s - \assigned to slave" This buer is reserved for writing. It may actually be being written at the moment or just marked as available for writing. n - \newest" This buer has just been written and contains the latest information. It is not being read at the moment. m - \assigned to master" This buer is being read by one or more processors. i - \idle" This buer is not being read or written and does not contain the latest data. The names of the master processors that are currently reading are also stored in the state. The VDM specication of [8] and [9] is concerned with various \data models" of MSMIE: the state of the device is modelled but not the slave and master processors nor the dynamic evolution of the system as they access the buers in parallel. This analysis concerns only the operations which modify the buer status ags. In the system as a whole, these operations are protected by a system of semaphores which allows each operation uninterrupted access to the state, and thus their behaviour is purely sequential. There are three such operations:
14 170 CHAPTER 6. VDM PROOFS IN PVS slave This operation is executed when a write nishes. The buer that was being written is given the status \newest" thereby replacing any other buer with this status. acquire This is executed when a read begins. The new reader name (passed as a parameter) is added to the set of readers and status ags are updated as appropriate. release This is executed when a read ends. The given reader name is removed from the set of readers and status ags are updated as appropriate. The precise description of these operations is left to the formal specication in the following section. We note, in passing, that the MSMIE protocol has the the undesirable property that it is possible for information ow from slave to master to be held up indenitely. This problem is dealt with in the original paper [17] by the use of timing constraints. The paper [11] suggests an improvement to the protocol in which the problem is avoided by the use of a fourth buer. This improved protocol is quite intricate, and is modelled in [8] by using non-standard extensions to VDM which provide a more concise means of expression than standard VDM-SL. In this report we restrict ourselves to standard VDM-SL specications and so do not treat the improved MSMIE protocol. The paper [8] explores several ways of specifying the MSMIE system in VDM with varying degrees of abstraction. These specications can be translated more or less \as is" into PVS, which can then be used to carry out proof obligations. The specications can be written in such away that some of the proof obligations are automatically generated by PVS, though it is still necessary to type in others by hand. The VDM specications of MSMIE which we show are in VDM-SL and therefore dier slightly from those in [8]. They were developed with the help of the IFAD VDM-SL Toolbox [14] The VDM Specication The specication uses an auxiliary function called count, which counts the number of occurrences of a given item in a sequence. functions
15 6.4. A SPECIFICATION EXAMPLE: MSMIE 171 @T! N count (s ss) 4 cases ss : []! 0 others! if hd ss = s then ](s tl ss) else ](s tl ss) end The possible values of the status ags are given via an enumerated type the type of the names of master processes is deferred. types Status = s j m j n j i MName = token The state records the status of each of the three buers, and the names of all currently reading master processes. These are represented by, respectively, a sequence of status values and a set of master names. The invariant captures constraints on the possible states that are reachable: there is exactly one buer assigned to the writing slave process at most one buer is currently being read, and at most one holds newest data that is not being read the set of readers is empty precisely when no buer is being read. In the initial state, one buer is assigned to the slave and the other two buers are marked as idle. state of b : Status ms : MName-set inv mk- (b ms) 4 len b =3^ count[status](s b) =1^ count[status](m b) 2f0 1g^ count[status](n b) 2f0 1g^ (count[status](m b) =0, ms = fg) end init s 4 s = mk- ([s i i] fg) The slave operation is executed when a slave process completes writing. The buer that has just been written, previously of status S, is given the status N reecting that it now contains the newest data. This buer replaces any other buer with the N status. The operation also selects one of the available buers and assigns to it status S, making it the new buer available for writing. operations
16 172 CHAPTER 6. VDM PROOFS IN PVS slave () ext wr b :(Status ) pre true post 8 i 2f1 2 3g ( (; b (i) =s ) b (i) =n) ^ ( (; b (i) =m ) b (i) =m) The acquire operation is executed when a master process is about to begin reading. The new reader's name, passed as a parameter, is added to the set of active readers, and status ags are updated as necessary. If there is already a buer being read, then the new reader also begins to read that buer and no status changes are needed. Otherwise it reads the buer with the newest data, status N, and the status of that buer is changed to M. acq (l : MName) ext wr b :(Status ) wr ms :(MName-set) pre (: (l 2 ms)) ^ (9 i 2f1 2 3gb (i) =n _ b (i) =m) post ms = (; ms [flg^ 8 i 2f1 (; 2 3g if b (i) =n ^ (; ms = fg then b (i) =m else b (i) = (; b (i) The release operation takes place when a master process has nished reading. The master's name is removed from the set of readers and buer ags reassigned as appropriate. If there are still other masters reading then the status ags do not need to be changed. Otherwise, the buer that has just been relinquished must have its status ag reassigned. There are two possibilities. If there is some other buer which was written while the read was taking place, and therefore has status N, then the released buer no longer contains the newest data and must have its status set to I. Otherwise, it still contains the freshest data and must have its status reset to N. rel (l : MName) ext wr b :(Status ) wr ms :(MName-set) pre l 2 ms
17 6.4. A SPECIFICATION EXAMPLE: MSMIE 173 post ms = (; ms nflg^ 8 i 2f1 2 3g if (; b (i) =m ^ ms = fg then b (i) 2fn ig^count[status](n b) =1 else b (i) = (; b (i) PVS Translation The VDM specication is represented as a PVS theory called msmie sigma2. The theory is parameterized over a non-empty type of master names. msmie_sigma2[mname : TYPE+] : THEORY BEGIN The theory begins by importing another theory containing denitions of functions on lists. The \count" function is dened within this imported theory. IMPORTING list_funs As in VDM, the possible values of the status ags are represented by anenumerated type. Status : TYPE = {Slave,Master,Newest,Idle} The state and invariant of the VDM specication are represented by a single (dependent) type in PVS. The denition is best understood in two parts. First, the state is represented as a record containing two elds: a list, b of Status values, and a set of master names, ms. The set of valid states is then represented by forming the subtype, sigma2, of all such records which satisfy the invariant. sigma2 : TYPE = {x : [# b : list[status], ms : setof[mname] #] ((length (b(x)) = 3) AND (count (Slave,b(x)) = 1) AND member(count(master,b(x)),{x:nat x=0 OR x=1}) AND member(count(newest,b(x)),{x:nat x=0 OR x=1}) AND ((count (Master,b(x)) = 0) <=> (ms(x) = emptyset)))} The initial state is dened as a record containing appropriate values and its type is explicitly constrained to be sigma2. When this denition is typechecked, PVS will automatically generate as a type-checking constraint (TCC) the condition that the
18 174 CHAPTER 6. VDM PROOFS IN PVS initial state satises the invariant. We shall look more closely at these TCCs in the next section. initial_sigma2 : sigma2 = (# b := (: Slave, Idle, Idle :), ms := emptyset #) For each operation, the precondition is represented as a predicate over the valid states (sigma2). The postcondition is represented as a predicate over pairs of valid states. The operation is then dened as a function which maps each value from the subtype dened by the precondition to some unspecied valid state which, when paired with the input value, satises the postcondition. Typechecking such a denition will cause PVS to generate a TCC stating that a suitable value for the post state does indeed exist. In other words, we are asked to show that the specied operation is feasible. Our rst example is the slave operation. The denitions of the pre- and postconditions resemble very closely the original VDM specication. One dierence is that there is no analogue in PVS to the frames in VDM, so that the fact that the variable ms has read-only status in the VDM specication must be explicitly stated in the PVS postcondition. pre_slave : [sigma2 -> bool] = LAMBDA (st:sigma2) : true post_slave : [(pre_slave),sigma2 -> bool] = LAMBDA (st:(pre_slave),st2:sigma2) : ((FORALL (i:{x:nat x=0 OR x=1 OR x=2}) : (nth(b(st),i) = Slave IMPLIES nth(b(st2),i) = Newest) AND (nth(b(st),i) = Master IMPLIES nth(b(st2),i) = Master)) AND (ms(st2) = ms(st))) The slave operation is then dened using the PVS choice operator choose. Our use of choose leads to a rather dierent interpretation of looseness from that adopted in VDM-SL. We defer discussion of this point until Section slave : [(pre_slave) -> sigma2] = LAMBDA (st:(pre_slave)) : choose({st2:sigma2 post_slave(st,st2)}) The specication of acquire is done similar. First the precondition and postcondition are dened as predicates. pre_acq : [MName ->[sigma2 -> bool]] = LAMBDA (l:mname)(st:sigma2) :
19 6.4. A SPECIFICATION EXAMPLE: MSMIE 175 (NOT member(l,ms(st))) AND (EXISTS (i:{x:nat x=0 OR x=1 OR x=2}) : (nth(b(st),i) = Newest OR nth(b(st),i) = Master)) post_acq : [l:mname -> [(pre_acq(l)),sigma2 -> bool]] = LAMBDA (l:mname)(st:(pre_acq(l)),st2:sigma2) : (ms(st2) = union(ms(st),singleton(l))) AND (FORALL (i:{x:nat x=0 OR x=1 OR x=2}) : IF nth(b(st),i) = Newest AND ms(st) = emptyset THEN nth(b(st2),i) = Master ELSE nth(b(st2),i) = nth(b(st),i) ENDIF) Next, the acquire operation is dened as a function which, when given a master name l and a state belonging to the type (pre_acq(l)), returns a nondeterministically chosen state in sigma2 such that the two states together satisfy the postcondition post_acq(l) acq : [l:mname, (pre_acq(l)) -> sigma2] = LAMBDA (l:mname, st:(pre_acq(l))) : choose({st2:sigma2 post_acq(l)(st,st2)}) The specication of the release operation is similar to that of acquire and is not described here Typechecking Constraints When the theory msmie_sigma2 is typechecked by PVS,a number of typechecking constraints (TCCs) are generated. These must be proved in order to demonstrate that the theory is well-typed. Simple TCCs can be handled by invoking an automatic TCC-prover, tcp, but more dicult ones must be proved interactively by the user. In the case of the theory msmie_sigma2, there are only 4 TCCs which are too dicult for tcp to prove. Interestingly, these TCCs correspond to the satisability proof obligations for the specication. We are required to show that the initial state satises the invariant, and that each of the three operations is feasible. Showing that the Initial State Satises the Invariant The rst TCC generated for msmie_sigma2 is shown below. It results from the fact that we have explicitly stated that the initial state, initial_sigma2, is of type sigma2 we are required to prove thatinitial_sigma2 satises the predicate which denes the subtype sigma2. In other words, we must show that the initial state satises the invariant. The proof is too dicult for tcp, but can be done quickly using the interactive prover. The main goal, which consists of a conjunction of 5 formulae, is split, making each conjunct into a separate subgoal. Each of these is
20 176 CHAPTER 6. VDM PROOFS IN PVS then proved by repeatedly expanding denitions until a statement is obtained which PVS recognises to be trivially true. initial_sigma2_tcc1: OBLIGATION ((length[status]((: Slave, Idle, Idle :)) = 3) AND (count[status](slave, (: Slave, Idle, Idle :)) = 1) AND member[nat](count[status](master, (: Slave, Idle, Idle :)), {x: nat x = 0 OR x = 1}) AND member[nat](count[status](newest, (: Slave, Idle, Idle :)), {x: nat x = 0 OR x = 1}) AND ((count[status](master, (: Slave, Idle, Idle :)) = 0) <=> (emptyset[mname] = emptyset[mname]))) Showing that the Operations Are Feasible To specify the operations we used the nondeterministic choice operator of PVS. For this to be correctly typed, PVS requires us to demonstrate that there exist possible candidates for the nondeterministically chosen values. In other words, wemust show that each operation is feasible. We show the statement of this proof obligation for the acquire operation. Given any master name l, and any state st within the type dened by the precondition, (pre_acq(l)), we must prove that the set of all states, st2, satisfying the postcondition post_acq(l)(st,st2) is nonempty. acq_tcc1: OBLIGATION (FORALL (l: MName, st: (pre_acq(l))): nonempty?[sigma2]({st2: sigma2 post_acq(l)(st, st2)})) This TCC has been proved interactively using PVS. The proof is unsurprising but not trivial: the user must supply a suitable candidate for the nondeterministic choice and then verify that all the various conditions imposed by the postcondition and the invariant are satised. We describe only the main highlights of the proof. After skolemizing, expanding denitions, and making some hidden hypotheses explicit, we are in a position where we may supply a possible candidate for the value that is nondeterministicallycho- sen. This is done using the tactic INST, whichisgiven two arguments: an integer representing the appropriate subgoal and a value for instantiation consisting of a record representing the state after the operation is carried out. In this case, the postcondition of the acquire operation happens to be very explicit so the calculation of the post state simply reects the postcondition. Note that identiers such as st!1 are skolem variables generated by PVS.
NASA Technical Memorandum 108991 (Revised) An Elementary Tutorial on Formal. Specication and Verication. Using PVS 2. Ricky W.
NASA Technical Memorandum 108991 (Revised) An Elementary Tutorial on Formal Specication and Verication Using PVS 2 Ricky W. Butler September 1993 (revised June 1995) NASA National Aeronautics and SpaceMore information
Edited by: Juan Bicarregui. With contributions from: Sten Agerholm. Bart Van Assche. John Fitzgerald. Jacob Frost. Albert Hoogewijs.
Proof in VDM: case studies Edited by: Juan Bicarregui With contributions from: Sten Agerholm Bart Van Assche John Fitzgerald Jacob Frost Albert Hoogewijs Cli Jones Peter Lindsay Savi Maharaj Brian MatthewsMore information
Introducing Formal Methods. Software Engineering and Formal Methods
Introducing Formal Methods Formal Methods for Software Specification and Analysis: An Overview 1 Software Engineering and Formal Methods Every Software engineering methodology is based on a recommendedMore information
CHAPTER 7 GENERAL PROOF SYSTEMS 1 Introduction Proof systems are built to prove statements. They can be thought as an inference machine with special statements, called provable statements, or sometimesMore information
Report T97:04 ISRN : SICS-T{97/04-SE ISSN : 1100-3154 Using Formal Methods A practical comparison between Z/EVES and PVS by Daniel Fredholm FDT 971204 Swedish Institute of Computer Science Box 1263, S-164More information
[Refer Slide Time: 05:10]
Principles of Programming Languages Prof: S. Arun Kumar Department of Computer Science and Engineering Indian Institute of Technology Delhi Lecture no 7 Lecture Title: Syntactic Classes Welcome to lectureMore information
programming languages, programming language standards and compiler validation
Software Quality Issues when choosing a Programming Language C.J.Burgess Department of Computer Science, University of Bristol, Bristol, BS8 1TR, England Abstract For high quality software, an importantMore information
Software Engineering
Software Engineering Lecture 04: The B Specification Method Peter Thiemann University of Freiburg, Germany SS 2013 Peter Thiemann (Univ. Freiburg) Software Engineering SWT 1 / 50 The B specification methodMore information
Mathematics for Computer Science/Software Engineering. Notes for the course MSM1F3 Dr. R. A. Wilson
Mathematics for Computer Science/Software Engineering Notes for the course MSM1F3 Dr. R. A. Wilson October 1996 Chapter 1 Logic Lecture no. 1. We introduce the concept of a proposition, which is a statementMore information
Verication by Finitary Abstraction Weizmann Institute of Sciences and Universite Joseph Fourier, Grenoble Fourth International Spin Workshop (SPIN'98) Paris 2.11.98 Joint work with: Y. Kesten Ben GurionMore information
Thomas Jefferson High School for Science and Technology Program of Studies Foundations of Computer Science. Unit of Study / Textbook Correlation
Thomas Jefferson High School for Science and Technology Program of Studies Foundations of Computer Science updated 03/08/2012 Unit 1: JKarel 8 weeks http://www.fcps.edu/is/pos/documents/hs/compsci.htmMore information
INTRODUCTION TO PROOFS: HOMEWORK SOLUTIONS STEVEN HEILMAN Contents 1. Homework 1 1 2. Homework 2 6 3. Homework 3 10 4. Homework 4 16 5. Homework 5 19 6. Homework 6 21 7. Homework 7 25 8. Homework 8 28More information
2.1.1 Examples of Sets and their Elements
Chapter 2 Set Theory 2.1 Sets The most basic object in Mathematics is called a set. As rudimentary as it is, the exact, formal definition of a set is highly complex. For our purposes, we will simply defineMore information
ML for the Working Programmer
ML for the Working Programmer 2nd edition Lawrence C. Paulson University of Cambridge CAMBRIDGE UNIVERSITY PRESS CONTENTS Preface to the Second Edition Preface xiii xv 1 Standard ML 1 Functional ProgrammingMore information
Peter V. Homeier and David F. Martin. email@example.com and email@example.com
A Mechanically Veried Verication Condition Generator Peter V. Homeier and David F. Martin Computer Science Department, University of California, Los Angeles 90024 USA firstname.lastname@example.com and email@example.com information
Automated Theorem Proving - summary of lecture 1
Automated Theorem Proving - summary of lecture 1 1 Introduction Automated Theorem Proving (ATP) deals with the development of computer programs that show that some statement is a logical consequence ofMore information
Chapter 4 Multi-Stage Interconnection Networks The general concept of the multi-stage interconnection network, together with its routing properties, have been used in the preceding chapter to describeMore information
MATH 289 PROBLEM SET 1: INDUCTION. 1. The induction Principle The following property of the natural numbers is intuitively clear:
MATH 89 PROBLEM SET : INDUCTION The induction Principle The following property of the natural numbers is intuitively clear: Axiom Every nonempty subset of the set of nonnegative integers Z 0 = {0,,, 3,More information
2. Methods of Proof Types of Proofs. Suppose we wish to prove an implication p q. Here are some strategies we have available to try.
2. METHODS OF PROOF 69 2. Methods of Proof 2.1. Types of Proofs. Suppose we wish to prove an implication p q. Here are some strategies we have available to try. Trivial Proof: If we know q is true thenMore information
Fundamentals of Mathematics Lecture 6: Propositional Logic
Fundamentals of Mathematics Lecture 6: Propositional Logic Guan-Shieng Huang National Chi Nan University, Taiwan Spring, 2008 1 / 39 Connectives Propositional Connectives I 1 Negation: (not A) A A T FMore information
key infrastructure-like applications. The central dierences between PolicyMaker and KeyNote are: { KeyNote predicates are written in a simple notation
KeyNote: Trust Management for Public-Key Infrastructures Matt Blaze 1 Joan Feigenbaum 1 Angelos D. Keromytis 2 1 AT&T Labs { Research 180 Park Avenue Florham Park, NJ 07932 USA fmab,firstname.lastname@example.com information
Verifying Specifications with Proof Scores in CafeOBJ
Verifying Specifications with Proof Scores in CafeOBJ FUTATSUGI, Kokichi 二 木 厚 吉 Chair of Language Design Graduate School of Information Science Japan Advanced Institute of Science and Technology (JAIST)More information
Induction. Mathematical Induction. Induction. Induction. Induction. Induction. 29 Sept 2015
Mathematical If we have a propositional function P(n), and we want to prove that P(n) is true for any natural number n, we do the following: Show that P(0) is true. (basis step) We could also start atMore information
Rigorous Software Development CSCI-GA 3033-009
Rigorous Software Development CSCI-GA 3033-009 Instructor: Thomas Wies Spring 2013 Lecture 11 Semantics of Programming Languages Denotational Semantics Meaning of a program is defined as the mathematicalMore information
M.Sc. program in mathematics INTRODUCTORY SET THEORY Katalin Károlyi Department of Applied Analysis, Eötvös Loránd University H-1088 Budapest, Múzeum krt. 6-8. CONTENTS 1. SETS Set, equal sets, subset,More information
Chapter 1: Key Concepts of Programming and Software Engineering
Chapter 1: Key Concepts of Programming and Software Engineering Software Engineering Coding without a solution design increases debugging time - known fact! A team of programmers for a large software developmentMore information
Deterministic Discrete Modeling
Deterministic Discrete Modeling Formal Semantics of Firewalls in Isabelle/HOL Cornelius Diekmann, M.Sc. Dr. Heiko Niedermayer Prof. Dr.-Ing. Georg Carle Lehrstuhl für Netzarchitekturen und NetzdiensteMore information
2. Basic Relational Data Model
2. Basic Relational Data Model 2.1 Introduction Basic concepts of information models, their realisation in databases comprising data objects and object relationships, and their management by DBMS s thatMore information
3. Mathematical Induction
3. MATHEMATICAL INDUCTION 83 3. Mathematical Induction 3.1. First Principle of Mathematical Induction. Let P (n) be a predicate with domain of discourse (over) the natural numbers N = {0, 1,,...}. If (1)More information
facultad de informática universidad politécnica de madrid
facultad de informática universidad politécnica de madrid On the Confluence of CHR Analytical Semantics Rémy Haemmerlé Universidad olitécnica de Madrid & IMDEA Software Institute, Spain TR Number CLI2/2014.0More information
Sets and functions. {x R : x > 0}.
Sets and functions 1 Sets The language of sets and functions pervades mathematics, and most of the important operations in mathematics turn out to be functions or to be expressible in terms of functions.More information
Higher-Order Logic. Specification and Verification with Higher-Order Logic
Higher-Order Logic Specification and Verification with Higher-Order Logic Arnd Poetzsch-Heffter Software Technology Group Fachbereich Informatik Technische Universität Kaiserslautern Sommersemester 2010More information
Module 7. Software Engineering Issues. Version 2 EE IIT, Kharagpur 1
Module 7 Software Engineering Issues Version 2 EE IIT, Kharagpur 1 Lesson 34 Requirements Analysis and Specification Version 2 EE IIT, Kharagpur 2 Specific Instructional Objectives At the end of this lesson,More information
Parametric Domain-theoretic models of Linear Abadi & Plotkin Logic
Parametric Domain-theoretic models of Linear Abadi & Plotkin Logic Lars Birkedal Rasmus Ejlers Møgelberg Rasmus Lerchedahl Petersen IT University Technical Report Series TR-00-7 ISSN 600 600 February 00More information
A Propositional Dynamic Logic for CCS Programs
A Propositional Dynamic Logic for CCS Programs Mario R. F. Benevides and L. Menasché Schechter {mario,firstname.lastname@example.com Abstract This work presents a Propositional Dynamic Logic in which the programs areMore information
Managing large sound databases using Mpeg7
Max Jacob 1 1 Institut de Recherche et Coordination Acoustique/Musique (IRCAM), place Igor Stravinsky 1, 75003, Paris, France Correspondence should be addressed to Max Jacob (firstname.lastname@example.com) ABSTRACTMore information
Theory of Computation Prof. Kamala Krithivasan Department of Computer Science and Engineering Indian Institute of Technology, Madras
Theory of Computation Prof. Kamala Krithivasan Department of Computer Science and Engineering Indian Institute of Technology, Madras Lecture No. # 31 Recursive Sets, Recursively Innumerable Sets, EncodingMore information
Chapter 1. Logic and Proof
Chapter 1. Logic and Proof 1.1 Remark: A little over 100 years ago, it was found that some mathematical proofs contained paradoxes, and these paradoxes could be used to prove statements that were knownMore information
Testing LTL Formula Translation into Büchi Automata
Testing LTL Formula Translation into Büchi Automata Heikki Tauriainen and Keijo Heljanko Helsinki University of Technology, Laboratory for Theoretical Computer Science, P. O. Box 5400, FIN-02015 HUT, FinlandMore information
Formal Engineering for Industrial Software Development
Shaoying Liu Formal Engineering for Industrial Software Development Using the SOFL Method With 90 Figures and 30 Tables Springer Contents Introduction 1 1.1 Software Life Cycle... 2 1.2 The Problem 4 1.3More information
Factoring & Primality
Factoring & Primality Lecturer: Dimitris Papadopoulos In this lecture we will discuss the problem of integer factorization and primality testing, two problems that have been the focus of a great amountMore information
Logic, Algebra and Truth Degrees 2008. Siena. A characterization of rst order rational Pavelka's logic
Logic, Algebra and Truth Degrees 2008 September 8-11, 2008 Siena A characterization of rst order rational Pavelka's logic Xavier Caicedo Universidad de los Andes, Bogota Under appropriate formulations,More information
Regular Expressions and Automata using Haskell
Regular Expressions and Automata using Haskell Simon Thompson Computing Laboratory University of Kent at Canterbury January 2000 Contents 1 Introduction 2 2 Regular Expressions 2 3 Matching regular expressionsMore information
CS 3719 (Theory of Computation and Algorithms) Lecture 4
CS 3719 (Theory of Computation and Algorithms) Lecture 4 Antonina Kolokolova January 18, 2012 1 Undecidable languages 1.1 Church-Turing thesis Let s recap how it all started. In 1990, Hilbert stated aMore information
MAT2400 Analysis I. A brief introduction to proofs, sets, and functions
MAT2400 Analysis I A brief introduction to proofs, sets, and functions In Analysis I there is a lot of manipulations with sets and functions. It is probably also the first course where you have to takeMore information
Software Engineering Reference Framework
Software Engineering Reference Framework Michel Chaudron, Jan Friso Groote, Kees van Hee, Kees Hemerik, Lou Somers, Tom Verhoeff. Department of Mathematics and Computer Science Eindhoven University ofMore information
Lecture 4 -- Sets, Relations, Functions 1
Lecture 4 Sets, Relations, Functions Pat Place Carnegie Mellon University Models of Software Systems 17-651 Fall 1999 Lecture 4 -- Sets, Relations, Functions 1 The Story So Far Formal Systems > Syntax»More information
A simple algorithm with no simple verication
A simple algorithm with no simple verication Laszlo Csirmaz Central European University Abstract The correctness of a simple sorting algorithm is resented, which algorithm is \evidently wrong" at the rstMore information
Z Styles for Security Properties and Modern User Interfaces
Z Styles for Security Properties and Modern User Interfaces Anthony Hall Praxis Critical Systems, 20 Manvers Street, Bath BA1 1PX email@example.com Abstract. This paper describes two new stylesMore information
Design by Contract beyond class modelling
Design by Contract beyond class modelling Introduction Design by Contract (DbC) or Programming by Contract is an approach to designing software. It says that designers should define precise and verifiableMore information
The Classes P and NP
The Classes P and NP We now shift gears slightly and restrict our attention to the examination of two families of problems which are very important to computer scientists. These families constitute theMore information
Mathematical Induction
Mathematical Induction In logic, we often want to prove that every member of an infinite set has some feature. E.g., we would like to show: N 1 : is a number 1 : has the feature Φ ( x)(n 1 x! 1 x) HowMore information
Notes. Sets. Notes. Introduction II. Notes. Definition. Definition. Slides by Christopher M. Bourke Instructor: Berthe Y. Choueiry.
Sets Slides by Christopher M. Bourke Instructor: Berthe Y. Choueiry Spring 2006 Computer Science & Engineering 235 Introduction to Discrete Mathematics Sections 1.6 1.7 of Rosen firstname.lastname@example.com IntroductionMore information
+ addition - subtraction and unary minus * multiplication / division mod modulo
Chapter 4 Basic types We examine in this chapter the Caml basic types. 4.1 Numbers Caml Light provides two numeric types: integers (type int) and floating-point numbers (type float). Integers are limitedMore information
What's Wrong With Formal Programming Methods? Eric C.R. Hehner
What's Wrong With Formal Programming Methods? Eric C.R. Hehner Department of Computer Science, University of Toronto, Toronto M5S 1A4 Canada The January 1991 issue of Computing Research News includes theMore information
Mechanical Verification of a Garbage Collector
Mechanical Verification of a Garbage Collector by Klaus Havelund FMPPTA 99 Talk by Sibylle Aregger Motivation handwritten proofs are error prone show approach to verify algorithm mechanically 2 ContentsMore information
We give a basic overview of the mathematical background required for this course.
1 Background We give a basic overview of the mathematical background required for this course. 1.1 Set Theory We introduce some concepts from naive set theory (as opposed to axiomatic set theory). TheMore information
MATH 55: HOMEWORK # SOLUTIONS ERIC PETERSON * 1. SECTION 1.5: NESTED QUANTIFIERS 1.1. Problem 1.5.8. Determine the truth value of each of these statements if the domain of each variable consists of allMore information
Prime Numbers. Chapter Primes and Composites
Chapter 2 Prime Numbers The term factoring or factorization refers to the process of expressing an integer as the product of two or more integers in a nontrivial way, e.g., 42 = 6 7. Prime numbers areMore information
CARDINALITY, COUNTABLE AND UNCOUNTABLE SETS PART ONE With the notion of bijection at hand, it is easy to formalize the idea that two finite sets have the same number of elements: we just need to verifyMore information
WHAT ARE MATHEMATICAL PROOFS AND WHY THEY ARE IMPORTANT? introduction Many students seem to have trouble with the notion of a mathematical proof. People that come to a course like Math 216, who certainlyMore information
3 Extending the Refinement Calculus
Building BSP Programs Using the Refinement Calculus D.B. Skillicorn? Department of Computing and Information Science Queen s University, Kingston, Canada email@example.com Abstract. We extend theMore information
A High Productivity Tool for Formally Veried Software Development
A High Productivity Tool for Formally Veried Software Development David Crocker and Judith Carlton Escher Technologies Limited, Mallard House, Hillside Road, Ash Vale, Aldershot GU12 5BJ, United Kingdom.More information
Sets. A set is a collection of (mathematical) objects, with the collection treated as a single mathematical object.
Sets 1 Sets Informally: A set is a collection of (mathematical) objects, with the collection treated as a single mathematical object. Examples: real numbers, complex numbers, C integers, All students inMore information
Encoding Mathematics in First-Order Logic
Applied Logic Lecture 19 CS 486 Spring 2005 Thursday, April 14, 2005 Encoding Mathematics in First-Order Logic Over the past few lectures, we have seen the syntax and the semantics of first-order logic,More information
The Generalized Railroad Crossing: A Case Study in Formal. Abstract
The Generalized Railroad Crossing: A Case Study in Formal Verication of Real-Time Systems Constance Heitmeyer Nancy Lynch y Abstract A new solution to the Generalized Railroad Crossing problem, based onMore information
Foundational Proof Certificates
An application of proof theory to computer science INRIA-Saclay & LIX, École Polytechnique CUSO Winter School, Proof and Computation 30 January 2013 Can we standardize, communicate, and trust formal proofs?More information
In mathematics you don t understand things. You just get used to them. (Attributed to John von Neumann)
Chapter 1 Sets and Functions We understand a set to be any collection M of certain distinct objects of our thought or intuition (called the elements of M) into a whole. (Georg Cantor, 1895) In mathematicsMore information
A set is a Many that allows itself to be thought of as a One. (Georg Cantor)
Chapter 4 Set Theory A set is a Many that allows itself to be thought of as a One. (Georg Cantor) In the previous chapters, we have often encountered sets, for example, prime numbers form a set, domainsMore information
(Refer Slide Time: 1:41)
Discrete Mathematical Structures Dr. Kamala Krithivasan Department of Computer Science and Engineering Indian Institute of Technology, Madras Lecture # 10 Sets Today we shall learn about sets. You mustMore information
Generating Test Cases from UML Specications by Aynur Abdurazik and Je Outt ISE-TR-99-09 May, 1999 Information and Software Engineering George Mason University Fairfax, Virginia 22030 Unlimited Distribution.More information
Chapter II. Controlling Cars on a Bridge
Chapter II. Controlling Cars on a Bridge 1 Introduction The intent of this chapter is to introduce a complete example of a small system development. During this development, you will be made aware of theMore information
Computing Concepts with Java Essentials
2008 AGI-Information Management Consultants May be used for personal purporses only or by libraries associated to dandelon.com network. Computing Concepts with Java Essentials 3rd Edition Cay HorstmannMore information
Verifying security protocols using theorem provers
1562 2007 79-86 79 Verifying security protocols using theorem provers Miki Tanaka National Institute of Information and Communications Technology Koganei, Tokyo 184-8795, Japan Email: email@example.com information
PL/SQL Overview. Basic Structure and Syntax of PL/SQL
PL/SQL Overview PL/SQL is Procedural Language extension to SQL. It is loosely based on Ada (a variant of Pascal developed for the US Dept of Defense). PL/SQL was first released in ١٩٩٢ as an optional extensionMore information
This asserts two sets are equal iff they have the same elements, that is, a set is determined by its elements.
3. Axioms of Set theory Before presenting the axioms of set theory, we first make a few basic comments about the relevant first order logic. We will give a somewhat more detailed discussion later, butMore information
Inference Rules and Proof Methods
Inference Rules and Proof Methods Winter 2010 Introduction Rules of Inference and Formal Proofs Proofs in mathematics are valid arguments that establish the truth of mathematical statements. An argumentMore information
MAT-71506 Program Verication: Exercises
MAT-71506 Program Verication: Exercises Antero Kangas Tampere University of Technology Department of Mathematics September 11, 2014 Accomplishment Exercises are obligatory and probably the grades willMore information
CHAPTER 3. Methods of Proofs. 1. Logical Arguments and Formal Proofs
CHAPTER 3 Methods of Proofs 1. Logical Arguments and Formal Proofs 1.1. Basic Terminology. An axiom is a statement that is given to be true. A rule of inference is a logical rule that is used to deduceMore information
Biinterpretability up to double jump in the degrees
Biinterpretability up to double jump in the degrees below 0 0 Richard A. Shore Department of Mathematics Cornell University Ithaca NY 14853 July 29, 2013 Abstract We prove that, for every z 0 0 with zMore information
Verification of Imperative Programs in Theorema
Verification of Imperative Programs in Theorema Laura Ildikó Kovács, Nikolaj Popov, Tudor Jebelean 1 Research Institute for Symbolic Computation, Johannes Kepler University, A-4040 Linz, Austria InstituteMore information
SYSTEMS AND SOFTWARE REQUIREMENTS SPECIFICATION (SSRS) TEMPLATE. Version A.4, January 2014 FOREWORD DOCUMENT CONVENTIONS
SYSTEMS AND SOFTWARE REQUIREMENTS SPECIFICATION (SSRS) TEMPLATE Version A.4, January 2014 FOREWORD This document was written to provide software development projects with a template for generating a SystemMore information
CBV Semantics (Draft) Navit Fedida, John Havlicek, Nissan Levi, and Hillel Miller Motorola, Inc. 7700 W. Parmer Lane Austin, TX 78729 13 January 2002 Abstract A precise denition is given of the semanticsMore information
DEGREES OF ORDERS ON TORSION-FREE ABELIAN GROUPS ASHER M. KACH, KAREN LANGE, AND REED SOLOMON Abstract. We construct two computable presentations of computable torsion-free abelian groups, one of isomorphismMore information
Myla Archer and Constance Heitmeyer. farcher, firstname.lastname@example.com. mechanical verication techniques is promising. Recently, we extended
Verifying Hybrid Systems Modeled as Timed Automata: A Case Study? Presented at HART '97, Grenoble, France, March 26-28, 1997 Myla Archer and Constance Heitmeyer Code 5546, Naval Research Laboratory, Washington,More information
Quotient Rings and Field Extensions
Chapter 5 Quotient Rings and Field Extensions In this chapter we describe a method for producing field extension of a given field. If F is a field, then a field extension is a field K that contains F.More information
Logic in Computer Science: Logic Gates
Logic in Computer Science: Logic Gates Lila Kari The University of Western Ontario Logic in Computer Science: Logic Gates CS2209, Applied Logic for Computer Science 1 / 49 Logic and bit operations ComputersMore information
Problems Encountered in the Machine-assisted Proof of Hardware? Paul Curzon University of Cambridge Computer Laboratory, Pembroke Street, Cambridge, UK. Email: email@example.com URL http://www.cl.cam.ac.uk/users/pc/More information
VDM vs. Programming Language Extensions or their Integration
VDM vs. Programming Language Extensions or their Integration Alexander A. Koptelov and Alexander K. Petrenko Institute for System Programming of Russian Academy of Sciences (ISPRAS), B. Communisticheskaya,More information
Coverability for Parallel Programs
2015 http://excel.fit.vutbr.cz Coverability for Parallel Programs Lenka Turoňová* Abstract We improve existing method for the automatic verification of systems with parallel running processes. The techniqueMore information
Model Driven Security: Foundations, Tools, and Practice
Model Driven Security: Foundations, Tools, and Practice David Basin, Manuel Clavel, and ETH Zurich, IMDEA Software Institute Thursday 1st, 2011 Outline I 1 Models Analysis. Types. 2 The Object ConstraintMore information
Appendix... B. The Object Constraint
UML 2.0 in a Nutshell Appendix B. The Object Constraint Pub Date: June 2005 Language The Object Constraint Language 2.0 (OCL) is an addition to the UML 2.0 specification that provides you with a way toMore information
Simulation-Based Security with Inexhaustible Interactive Turing Machines
Simulation-Based Security with Inexhaustible Interactive Turing Machines Ralf Küsters Institut für Informatik Christian-Albrechts-Universität zu Kiel 24098 Kiel, Germany email@example.com information
Scalable Automated Symbolic Analysis of Administrative Role-Based Access Control Policies by SMT solving
Scalable Automated Symbolic Analysis of Administrative Role-Based Access Control Policies by SMT solving Alessandro Armando 1,2 and Silvio Ranise 2, 1 DIST, Università degli Studi di Genova, Italia 2 SecurityMore information
Automated Program Behavior Analysis
Automated Program Behavior Analysis Stacy Prowell email@example.com March 2005 SQRL / SEI Motivation: Semantics Development: Most engineering designs are subjected to extensive analysis; software isMore information
A Systematic Approach. to Parallel Program Verication. Tadao TAKAOKA. Department of Computer Science. Ibaraki University. Hitachi, Ibaraki 316, JAPAN
A Systematic Approach to Parallel Program Verication Tadao TAKAOKA Department of Computer Science Ibaraki University Hitachi, Ibaraki 316, JAPAN E-mail: firstname.lastname@example.com Phone: +81 94 38 5130More information
Jieh Hsiang Department of Computer Science State University of New York Stony brook, NY 11794
ASSOCIATIVE-COMMUTATIVE REWRITING* Nachum Dershowitz University of Illinois Urbana, IL 61801 N. Alan Josephson University of Illinois Urbana, IL 01801 Jieh Hsiang State University of New York Stony brook,More information
Master Thesis no. 442
Clean Prover System A tool for interactively and automatically proving properties of functional programs Maarten de Mol firstname.lastname@example.com Master Thesis no. 442 University of Nijmegen (KUN) August 12,More information
Specification and Analysis of Contracts Lecture 1 Introduction
Specification and Analysis of Contracts Lecture 1 Introduction Gerardo Schneider email@example.com http://folk.uio.no/gerardo/ Department of Informatics, University of Oslo SEFM School, Oct. 27 - Nov.More information
2 Formal User Modelling There are, broadly speaking, two main approaches to formal reasoning about the usability of systems. One approach is to focus
Reasoning about Order Errors in Interaction Paul Curzon and Ann Blandford School of Computing Science, Middlesex University, London, UK fp.curzon,email@example.com Abstract. Reliability of an interactiveMore information


text:
Wet 'n Wild is generally considered to be the first major water park in the United States. Opened in 1977 by George Millay, one of the founders of SeaWorld, Wet 'n Wild has been in continuous operation ever since. Millay actually received the first ever Lifetime Achievement Award from the World Waterpark Association, which named him "Father of the Waterpark."
After the SeaWorld chain was sold off to textbook publisher Harcourt Brace Jovanovich in 1976, Millay focused on ownership of Wet 'n Wild. Wet 'n Wild branches opened in both Garland and Arlington, Texas as well as Las Vegas, Greensboro, North Carolina, and three locations in Brazil. Gradually the other locations were sold and many of them closed permanently or were completely re-themed. This left Millay with only the Orlando park. In 1998, Millay finally sold his last park to Universal Orlando and retired to San Diego. George Millay passed away on February 7, 2006.
One of the reasons for Wet 'n Wild's enduring success is the park's willingness to change with the times. The park that became the model for the modern water park had a lot to live up to. Wet 'n Wild's early success laid the foundation for imitators everywhere, all competing to be the biggest and the best and the most well-known. Wet 'n Wild has done an admirable job of growing and changing over the years in order to remain competitive, and still manages to hold its own against such gargantuan competitors as Disney's Typhoon Lagoon and Blizzard Beach. Indeed, Wet 'n Wild continues to win awards, such as its recent title as America's Number One Water Park given by Amusement Business magazine.
Part of the secret to Wet 'n Wild's success is the excellent blend of attraction types. World-class thrill slides exist harmoniously with more laid back attractions, and the children's area is top notch. You should, of course, be a swimmer to visit a water park, but Wet 'n Wild offers a full day of fun for those who do not feel comfortable with the high-speed, high-energy thrill rides. Thrill seekers can enjoy a completely different experience, challenging themselves again and again on Wet 'n Wild's most punishing attractions.
Thrill Rides:
For pure thrills and spills, advance word has it that Brain Wash (opening spring 2007) will top them all. Tubes holding 2 or 4 riders will experience a 53 foot vertical drop into the center of a spiraling tornado. The funnel is 65 feet high, and you will experience every twist and turn as you make your way down. This will truly be the new ride to beat in the water park world. Height restrictions have not yet been released.
Don't miss Der Stuka. This six story solo slide is all about the speed with a nearly vertical drop that transitions into a gliding runway. Riders must be at least 48" tall.
Another solo ride, The Storm, may have been the inspiration for Brain Wash. The Storm sends you down an elevated chute into a spinning, turning bowl below. Minimum height is 48".
Mach 5 is also designed for solo riders. Be sure to ride all three of the twisting and turning head first slides, as each follows a different course.
In The Bomb Bay, you are the bomb! A trap door opens suddenly underneath you, launching you down 75 feet of nearly vertical terror. Height requirement for Bomb Bay is 48".
In The Blast, a two person raft careens through a broken pipeline. You must be able to work together to control your raft, and both riders must be strong swimmers.
Family Friendly:
Disco H2O is a true blast from the past. Your four person tube will careen through a groovy world of light and sound. The slide is great, but the true thrill comes from the funky Disco overlay. Riders must be 36" if accompanied by an adult, or 48" to ride solo.
The Surge places four riders in a raft for a thrilling 600 feet of banked turns, sudden dips and surprises. Riders must be 36" if accompanied by an adult or 48" to ride alone.
Take the plunge into the Black Hole. Covering 500 feet of track through total darkness, this two person tube ride is heavy on the thrills. Riders need be only 36" to ride with an adult or 48" to ride unaccompanied. Make sure, however, that your little one is up to the thrills. Even some adults become unnerved by the combination of water, tunnels, and darkness.
The Flyer is a four person toboggan ride focusing on tight curves and hairpin turns. Riders must be 36" tall to ride with an adult or 48" to ride alone.
The Bubba Tub brings your family closer together on four person tubes that careen through a six story triple drop. The height requirement is 36" to ride with an adult or 48" to ride alone.
Easy and Relaxed:
Wet 'n Wild's Lazy River replicates old Florida with boat docks, aged billboards and a variety of waterfalls. Grab a tube and float the afternoon away.
In the Wave Pool, comfortable four foot waves roll gently past as you bob and bounce. Play under the breathtaking waterfall or grab a comfortable poolside seat to relax and enjoy the sun.
Beach Volleyball courts are also available for your convenience
Kids Only:
Wet 'n Wild boasts one of the best children's areas in any water park. Kids' Park features miniaturized versions of Wet 'n Wild's most popular slides. This keeps little ones from being jealous or upset that their older siblings can ride certain things, and also builds confidence in the water. Only children under 48" tall are permitted to ride. There is also a play area with an inflatable bubble bounce known as Bubble Up and other child-friendly features.
Water Sports:
Visit the Wake Zone for Knee Skiing, Wake Skating, and the mysterious "The Wild One." Wake Zone attractions require riders to be 56" tall (51" for The Wild One) and strong swimmers. Additional fees may apply.
Wet 'n Wild is a wonderful experience for those of all ages and levels of water experience. Prices are quite reasonable and there are an incredible number of price specials running at any given time. No Orlando vacation is complete without a visit to the water park that started it all, Wet 'n Wild.

subset: commoncrawl


text:
Sam Allardyce likes a good defensive midfielder, as he showed when he decided he wanted Steven N'Zonzi at Everton when the France international was having problems with then Sevilla manager Eduardo Berizzo.
With that situation now mostly resolved since the arrival of Vincenzo Montella and the former Blackburn man not leaving for much less than his €40m release clause, it appears the attention has turned elsewhere.
This is what Foot Mercato are reporting on Tuesday, as they claim Everton are one of two clubs keeping tabs on Petrus Boumal.
The 24-year-old defensive midfielder, who spent his early years in France with Sochaux, recently transferred to Russian Premier League club FC Ural from CSKA Sofia.
Since his arrival, Boumal has started 12 of a possible 16 games, and is quickly making a name for himself in the team.
Foot Mercato explain that Everton could make a move as early as this summer if Idrissa Gueye ends up moving to a bigger club come the end of the season.
RC Genk in Belgium are reported to have tried a €2m offer in January, quickly rejected by the Russian side.
Guess that means Everton will need to pay more than that if they want to sign him.


text:
Today, Nelo takes the floor to give us her Conference report from the concluded NBA AGC 2016 held in Port Harcourt. So its Nelo on the Beat!
By Thursday, 18th of August 2016, I had already arrived Port Harcourt for the 56th AGC of the NBA scheduled for 19th to 26th of August 2016. The next day being Friday, I went along with a friend to the Judiciary Complex, for the collection of conference materials, but we were asked to return on Saturday (20th August, 2016) afternoon.
On our return on Saturday, there was a bit of a crowd, but I managed to get my name tag. Unfortunately, my friend who had registered early for the AGC could not get hers. She was asked to put down her name and return the next day. It was "made" for her then. The other material, (a school bag with a face towel in it) was not available; we were asked to return on Sunday.
We were informed that a welcome party was to be held for Conferees by 6pm, on that same Saturday, Eddy's Wine Bar, GRA Port Harcourt. I attended with two of my friends, though the venue was scanty compared to the crowd that we met at the collection point for name tags. I was only lucky to have quick access to information since my friend was a member of the Port Harcourt branch and a subcommittee of the Local Organising Committee (LOC). Many conferees were not so lucky and missed out on the welcome party.
The opening ceremony followed on Sunday at the Conference Venue; the Civic Center Port Harcourt. Attendance was high with some dignitaries present. The Governor of Rivers State, Nyesom Wike Esq. gave a welcome speech which I considered politically flavoured and controversial. He accused the ruling party of disrespect for the rule of law and cited the prevention of his party from holding its last convention in Port Harcourt as an example.
Thereafter was the key Note speaker spoke the Rwandan Attorney General and Minister of Justice, Mr. Busingye Johnson. The Highlight of the day for most of us was when Timaya mounted the stage. We sang and danced until he left which I thought was quite early, lol. I guess I enjoyed it that much.
On Monday, most of us who opted to get our material from the conference ground had not gotten any. The news on Sunday was that it was not available. By Monday morning, it was available but the crowd was much in addition to the fact that the conference had begun in earnest. I did what was reasonable by forgoing the material that was not forthcoming and head to Civic Center to attend the morning session, which was on "Growing Nigeria's Economy Beyond Oil and Gas". It was quite insightful section.
The conference sessions went on without a hitch; morning sessions were followed by lunch breaks after which the afternoon parallel sessions ran from 2pm to 4.30pm. Conferees were at liberty to attend any afternoon session of their choice. On Tuesday, I attended one of the parallel sessions with the topic, "Enforcing Laws Protecting Women and Children: Issues and Challenges." The session caught my fancy as it touches the core of my passion for women's right, and I was inspired by the lead speaker, Nana Oye Lithur who is the Ghanaian Minister of Gender, Children and Social Protection. She gave an elaborate presentation on the development of the Laws in Ghana to fit in recent happenings as regards the rights of women.
I can say that save for the organization which was well below standard, the conference content was really rich, and we had well seasoned speakers who took on their topics with mastery. Mr. Solomon Arase, the former Inspector General of Police alongside many other speakers of the conference, was quite impressive.
On organization of the conference, I really felt uncared for by the executive of the NBA who hosted the 2016 AGC. The former President Mr. Augustine Alegeh SAN was unconcerned about the complaints of conferees on the shortage of materials. He had even in response to a senior lawyer's complaint on the issue retorted that "the members did not attend the NBA conference to get materials."
His response was greeted by a disapproving uproar from the conferees in the Civic Center, but the president was unperturbed by it. I overheard some members saying the president's attitude could be because his tenure was over. I had no doubt they could be right.
Another low point for the AGC was the announcement of a banquet organized by the governor at the Governor's Lodge for conferees. However a limited number of invitation cards were available and I could not attend like many others.
Another banquet organized by the wife of the governor Justice Suzzette Eberechi Nyesom Wike, was marred non availability of invitation cards and thus like the earlier banquet I could not attend. I had no doubt that the limited invitation cards were due to the limited space in the banquet hall.
I got the conference materials one day before the last day of the AGC. My 4 friends and I were not ready to forego any of the AGC sessions to struggle for the materials. The materials could have been useful guides if we had received them before the AGC commenced.
The last straw that broke the camel's back was the way the general farewell dinner was organized or better still disorganized. The hall was arranged in a round table pattern and almost half of the conferees could not be accommodated with the sitting arrangement. Many conferees were denied access into the congested and stuffy dinner hall.
Respite came when the door was opened for the rest of the members to pick a chair and sit at the back. To further bad insult to injury, members had to wait from 7pm to past 10pm for the President of NBA, and Governor Wike to arrive before dinner could be served, upon which they both left immediately.
As at 11pm worn out and frustrated conferees were still queuing up for food. I had found consolation in taking pictures with willing colleagues in the whole melee. I guess my friends on my social media platforms were thinking I was having a time of my life with the captivating pictures I was sharing online.
I actually had a few good moments, like when Tuface Idibia performed on Wednesday Night, it was so exciting to watch my best artist perform on stage. I reunited with my old friends and new ones I had gotten friendly with on social media, it wonderful seeing them all and taking photos. It was great to be surrounded by professional colleagues for a week; connecting, socializing and sharing knowledge and experiences.
I decided I will attend next year and more years to come for the good reasons while I look forward to a better organized AGC in the future by the new Executive of the NBA. I hope they stumble upon some of the numerous assessments made concerning this year's AGC, and improve on it.
Long Live Federal Republic of Nigeria
Long Live Nigerian Bar Association.
Chinelo Oge Akorah is a Lawyer based in Asaba, Delta State Nigeria. She could be reached on email@example.com. She blogs on http://chineloakorah.blogspot.com.ng


text:
Scott Bentley
This guy gets paid doing nothing. Except being on his phone.
he's overall a very funny and humorous person, he's really great with students. it may seem great having him as a teacher because he barely teaches, i do recommend switching out of his class though. your most likely going to fail in the next year if you don't have him.
He's a great teacher for two reasons; If you don't care about the class or learning you can just sit on your phone all class but you also have the choice to learn.
He is so bad, he does not teach, why is he even a teacher?
People say all you do is watch movies in his class but I will tell you first hand he is very knowledgable and you can learn and gain a lot by listening to him it's just most kids don't and he doesn't wanna nag for them to listen you can either listen and learn or not listen goof off and not learn up to you he's a great teacher !!!
He doesn't do his job at all! Every class we watch Mythbusters and Hollywood movies such as Contagion and osmosis jones! We never use our text books and we've had 15 substitute teachers this year! I've learned nothing! I would not recommend him as a teacher! He's the worst!
It's amazing how one guy can waste an entire school year on weird science videos he finds on the Internet, but somehow he manages. I'll be the first to admit that I didn't learn any science, but his class was fun and always something to look forward to. The easy A was great to. All in all, if you want a lovable, awkward nerdy teacher, who doesn't make eyecontact with anyone ever, he's the guy.
Holy! His girlfriend told me the cops are on him for molesting a child. Watch out kids, this guy is bad news.
He is a nice guy who makes lots of puns; however, he doesn't teach much and usually plays a video for every class.
Did labs and watched videos the whole year. He doesn't teach and we had one test the whole year and everyone got 36/40. He doesn't mark anything and it's an easy class, but I went into Science 10 with no knowledge whatsoever because of Bentley. He's nice, but he never makes eye contact with you. He's helpful when you need to ask about labs, but he doesn't teach much. The final exam was the same as the review package he gave us. If you get him, I would transfer. Would not recommend.
Watched videos most of the time and it was fantastic!
Very kind teacher who encouraged my child to pursue a career in radiology.
Only thing I learned was that the Bentley I'd not only a car but a teacher with many puns and a beautiful voice. He should run away to a far away land and sing opera. Love this guy.
Great teacher; he is the reason why I've decided to pursue a biology major after I graduate this year. Sure he doesn't give tests or assign homework, but regardless, I was still taught well enough to be able to draw upon my biology knowledge in biology 12!
he's a super nice guy but doesnt teach much. he really knows what he's talking about though, and he can explain if you ask him to. the class is super easy and there is rarely ever homework or tests
All i have to say is that Mr. Bentley is the best teacher in argyle.. hands down! there's just no competition... i love this guy
Mr. Bently is a truly amazing teacher, alwase fun and happy and full of shinanagins. Very helpful and thoughtful, I can see him being an amazing father. I was absolutly devistated when he was sick for
great teacher know his stuff,hes always got that answer to your question and if he doesn't he will look it up, is alway there to offer help. A
I can see Bentley being a great father figure. Caring, helpful, and knowledgeable in his concern and love for the environment. He's awesome!
Mr. Bently is that best!! i love his movies and i love how he tries rlly hard to make us laugh XD
Bennett is hands down the most entheusiastic and helpful teacher I've ever had. He cares a lot about the students and he has very clear lessons which are easy to understand and usually really fun.
easy, cool videos and jokes just study the notes he gives before tests
Hes a great teacher, if I didnt have him I wouldn't have had grade 11 or 12 science to graduate.
As long as you can study on your own this class is awesome. Even if you can't you'll probably still get by with a B or a C+. The movies can get boring but I'm glad I didn't get a different teacher!
He's nice, a great teacher if you're good at studying on your own. I do admit he can go off topic a little and sort of get a little vague, but overall, he's a good teacher :)
nice guy, really funny but needs to watch show less movies and actually teach
hes so funny cause he thinks hes funny but his jokes are always so bad, but hes a good teacher
i found the tests easy and the class was the best him and his joke
VERY unhelpful..Avoid no matter what. He just reads over his notes and expects you to know everything. Easy though.
Nice guy. Had him every year except grade 10. Bio 11 was definately my favourite. We watched Army of Darkness on the last day of class! HAHA! Good times.
mr bentley's awsome, really corny jokes thou....its not rocket science, it's brain surgery.....working hard?or hardly working?
hah I Live mr Bently! hes sooooo nice! his jokes are kinda corny though.......
he's kinda funny.. well he thinks he is but overall he's nice
He was the best math teacher I ever had. Mostly he teaches science, but I had him for Math 9 Honours. He makes me want to pay attention :)
mr.Bently is the greatest science teacher ever in BC.HE Rox.! if u don't have him ur sooo unluckey he's sooooo funny and his stories are hilarius.
mr.bently is the best but i dunno noe yet he my first science. hes really easy on science tests and he wastes good class time
Super nice teacher! It can get kind of boring in his class sometimes but he tries really hard to make it fun and hes really funny and hes really interested in helping his students
pretty boring class except the random jokes and the tests are way too hard
An overall great guy. HE GAVE US CANDY ALL THE TIME... and always made math really fun ;x Loved his random stories too.
Mr. Bentley is such a nice guy. I love his stories and his randomness. ^__^
haha mr. bentley rules! he always gets of topic and if you're quiet he says silly things to amuse himself. it's so much fun! good quotes too
Bentley is the man! However I'm not so sure about his unhealthy passion for the Flames. Great hockey talk made Math bearable and class entertaining. Lupe rocks!


text:
― Mark Twain
I subscribe to Wisdom 2.0. What on earth is this?
Well, Wisdom 2.0's tag line is: The intersection of wisdom and technology
It seeks to address the great challenge of our age: to not only live connected to one another through technology, but to do so in ways that are beneficial to our own well-being, effective in our work, and useful to the world. I listened to a talk today from a wonderful person, called Elle Luna. She wrote an article called:
The Crossroads of Should and Must
This is a story about two roads — Should and Must. It's a pep talk for anyone who's chosen Should for far too long — months, years, maybe a lifetime — and feels like it's about time they gave Must a shot.
If you can take 30 minutes to watch the video, then I'd urge you to do so. If you only have time to read the article she wrote, read it. It might just change your life....
The video can be found at:
The article can be found at:
Further videos from this years Wisdom 2.0 conference can be found at:


text:
Jaden Smith Brings a Very Large Camera Out to Lunch
Jaden Smith carries what appears to be an expensive and very large camera out for lunch on Sunday (January 4) in Calabasas, Calif.
The 16-year-old entertainer brought the camera to Le Pain Quotidien for his afternoon meal that day – perhaps he was having a photo shoot in the cafe!
PHOTOS: Check out the latest pics of Jaden Smith
"People Think They Have To Choose." Jaden recently tweeted that same day to his over five million followers.
20+ pictures inside of Jaden Smith carrying his camera out to lunch..