text:
An Evening at Ninety Acres, Natirar Estate: Peapack-Gladstone, NJ
Spoiled Rotten. That's the words that best describe me after my recent excursion to Ninety Acres at Natirar. Before I carry myself back and away with the dining experience, I'll let you know how I ended there. Natirar is a sprawling 500 acre property and estate in Peapack, NJ that houses a cooking school, farm, meetings and event space, and a fine dining restaurant, Ninety Acres. The property is the embodiment of countryside elegance. The restaurant is reserved for luxurious nights out with an expensive menu, extensive wine list, and elaborate farm to table fare. Previous to my most recent visit I had visited the restaurant one other time for a special birthday dinner date with my now husband. However; our friends know us all too well and more than one of our wedding guests thought to give us a gift card to this estate to use to enjoy the finer foods in life. We've managed to make it six whole months without finding the time to make a reservation. But, we had an empty weekend and we finally ceased the opportunity.
$200 Starbucks Giftcard Giveaway
Hey Everyone-I bringing you a little holiday cheer and something to keep you warm today. Enter below for a chance to win a $200 Starbucks Giftcard. Check out some of the other awesome bloggers involved too! Good Luck!
Sun Basket Meal delivery-Why You Should Try and $30 off!
The New Year is almost here and what better time to start fresh?! Part of me is sad that I no longer have the excuse of Christmas celebrations to stuff myself and indulge in gluttonous activities. However; the other half of me is excited to get back on track with my daily eating and exercising routines. I am going to resolve to be a little more conscious of what I am cooking throughout the week. Last year, leading up to the wedding I had become a pro at this activity. Unfortunately, I let the post-wedding bliss get to my head and my stomach a little too much this fall!
Prosciutto and Blue Cheese Wrapped Pear Bites
I'm keeping the holiday preparations theme going with another crowd pleasing recipe. In my family, the holidays are all about appetizers! On Christmas Eve we do an entire meal of just appetizers with our extended family. Essentially its one large cocktail hour with Christmas cookies to follow! Every year we have our standard recipes that must ALWAYS be present for it to be a Somers (My maiden name) holiday. While my mom's cranberry meatballs and my uncle's spicy calamari marinara never leave the list, I try to come up with inventive new ones each year to tack on to the menu. This year I'll be bringing my stuffed mushrooms that I shared a few weeks back and today recipe, prosciutto and blue cheese wrapped pears.
Workman's Friend, The Everybody Pub- Charlotte, NC
Hi Everyone!
Last month I scooted back down to Charlotte for a weekend to visit my bestie. I have a feeling it's the beginning of a beautiful friendship with the Queen City (As Charlotte is often referred to). For those of you looking to travel there, just check back every few months to find more reviews and travel tips. And for those of you reading from the Charlotte area looking for great spots to try out, I'm happy to share your city! If you missed out on my big foodie find from my September trip, here it is (Midwood Smoke House).
Wild Rice and Chicken Sausage Stuffed Acorn Squash
I've been doing a variety of meal delivery services in the past few months (More to come on these in another post). I originally ordered them because I got a great deal on the first week's subscription and it took the brainwork out of cooking for half of the week. While the convenience is still a major contributing factor for why I continue, one of the other many benefits is cooking inspiration. I have have learned more about cooking techniques with specific ingredients. I have used recipe components in other ways that I thought to in the past. I have also worked on some recipes with ingredients I haven't used at all in the past. Today's recipe stems from one of those experiences.


text:
Our selection of luxury family holidays to the Seychelles have been hand selected by our travel specialists to ensure that they are suitable for adults and children of all ages.
Submerged in the Indian Ocean, this stunning group of islands is adorned with palm-fringed beaches, warm turquoise waters and exotic flora and fauna. Secluded yet sophisticated with excellent restaurants, a range of luxurious accommodation, and a playground so stunningly beautiful you will not be disappointed with a luxury family holiday in the Seychelles.
At Western & Oriental we feature a wonderful collection of family friendly resorts spread across several of the Seychelles unique islands. Each offers a range of excellent facilities for families of all ages, as well as an abundance of watersports activities, including kayaking, snorkelling, diving, windsurfing and much more.
With many of the islands only a short flight away, island-hopping is a great way to fully appreciate the Seychelles; make a day of it or plan an overnight tour, selecting two or three of your favourite islands for the family to explore.
For those who like to plan ahead we offer all inclusive holidays to Seychelles which are suitable for the whole family.
To plan an unforgettable luxury family holiday in the Seychelles call our family travel specialists today.
Read more about Seychelles Family Holidays

subset: commoncrawl


text:
ПЕРИОДИЧНОСТЬ ИЗДАНИЯ: 1 раз в 2 месяцаThe magazine is published since 1884. Publishes materials on the diagnosis and treatment of eye diseases, hygiene of view, the prevention of eye diseases, eye care organizations population. Presented in the following databases: RISC, MEDLINE, Ulrich's Periodicals Directory. Included in the list of HAC.
Publication frequency: 1 time in 2 months


text:
Peter V. Homeier and David F. Martin. and
- Cuthbert Benson
- 2 years ago
- Views:
1 A Mechanically Veried Verication Condition Generator Peter V. Homeier and David F. Martin Computer Science Department, University of California, Los Angeles USA and Verication Condition Generator (VCG) tools have been eective in simplifying the task of proving programs correct. However, in the past these VCG tools have in general not themselves been mechanically proven, so any proof using and depending on these VCGs might not be sound. In our work, we dene and rigorously prove correct a VCG tool within the HOL theorem proving system, for a standard while-loop language, with one new feature not usually treated: expressions with side eects. Starting from a structural operational semantics of this programming language, we prove as theorems the axioms and rules of inference of a Hoare-style axiomatic semantics, verifying their soundness. This axiomatic semantics is then used to dene and prove correct a VCG tool for this language. Finally, this veried VCG is applied to an example program to verify its correctness. 1. INTRODUCTION The most common technique used today to produce quality software without errors is testing. However, even repeated testing cannot reliably eliminate all errors, and hence is incomplete. To achieve a higher level of reliability and trust, programmers may construct proofs of correctness, verifying that the program satises a formal specication. This need be done only once, and eliminates whole classes of errors. However, these proofs are complex, full of details, and dicult to construct by hand, and thus may themselves contain errors, which reduces trust in the program so proved. Mechanical proofs are more secure, but even more detailed and dicult. One solution to this diculty is partially automating the construction of the proof by a tool called a Verication Condition Generator (VCG). This VCG tool writes the proof of the program, modulo a set of formulas called verication conditions which are left to the programmer to prove. These verication conditions do not contain any references to programming language phrases, but only deal with the logics of the underlying data types. This twice simplies the programmer's burden, reducing the volume of proof and level of proof, and makes the process more eective. However, in the past these VCG tools have not in general themselves been proven, meaning that the trust of a program's proof rested on the trust of an unproven VCG tool. In this work we dene and rigorously prove correct a VCG within the Higher Order Logic (HOL) theorem proving system [Gordon 93], for a standard while-loop language that has a feature not usually treated: expressions with side eects. Expressions with side effects occur in the programming languages C and C++, and are therefore of practical interest. We prove that the truth of the verication conditions returned by the VCG suce to verify the asserted program submitted to the VCG. This theorem stating the VCG's correctness then supports the use of the VCG in proving the correctness of individual programs with complete soundness assured. The VCG automates much of the work and detail involved, relieving the programmer of all but the essential task of proving the verication conditions. This enables proofs of programs which are both eective and trustworthy. 2. PREVIOUS WORK In this paper, we dene a \veried" verication condition generator as one which has been proven to correctly produce, for any input program and specication, a set of verication conditions whose truth implies the consistency of the program with its specication. Preferably, this verication of the VCG will be mechanically checked for soundness, because of the many details and deep issues that arise. Many VCGs have been written but not veried; there is then no assurance that the verication conditions produced are properly related to the original program, and hence no security that after proving the verication conditions, the correctness of the program follows. Gordon's work below is an exception in that the security is maintained by the HOL system itself. In 1973 Larry Ragland veried a verication condition generator written in Nucleus, a language Ragland invented to both express a VCG and be veriable [Ragland 73]. This was a remarkable piece of work,
2 2 Peter V. Homeier and David F. Martin well ahead of its time. The VCG system consisted of 203 procedures, nearly all of which were less than one page long, which gave rise to approximately 4000 verication conditions. The proof of the generator used an unveried VCG written in Snobol4. The verication conditions it generated were proven by hand, not mechanically, but substantially veried the VCG. In 1975 Igarashi, London, and Luckham gave an axiomatic semantics for a subset of Pascal, and described a VCG they had written in MLISP2 [Igarashi 75]. The soundness of the axiomatic semantics was veried by hand proof, but the correctness of the VCG was not rigorously proven. The only mechanized part of this work was the VCG itself. Michael Gordon in 1989 did the original work of constructing within HOL a framework for proving the correctness of programs [Gordon 89]. He introduced new constants in the HOL logic to represent each program construct, dening them as functions directly denoting the construct's semantic meaning. This is known as a \shallow" embedding of the programming language in the HOL logic. The work included dening verication condition generators for both partial and total correctness as tactics. This approach yielded tools which could be used to soundly verify individual programs. However, the VCG tactic he dened was not itself proven. If it succeeded, the resulting subgoals were soundly related to the original correctness goal by the security of HOL itself. Fundamentally, there were certain limitations to the expressiveness and proven conclusions of this approach, as Gordon himself recognized: P[E=V] (substitution) is a meta notation and consequently the assignment axiom can only be stated as a meta theorem. This elementary point is nevertheless quite subtle. In order to prove the assignment axiom as a theorem within higher order logic it would be necessary to have types in the logic corresponding to formulae, variables and terms. One could then prove something like: ` 8P EV: Spec (Truth (Subst (P; E; V )); Assign (V; Value E); Truth P ) It is clear that working out the details of this would be a lot of work. [Gordon 89] In 1991, Sten Agerholm [Agerholm 92] used a similar shallow embedding to dene the weakest preconditions of a small while-loop language, including unbounded nondeterminism and blocks. The semantics was designed to avoid syntactic notions like substitution. Similar to Gordon's work, Agerholm dened a verication condition generator for total correctness specications as an HOL tactic. This tactic needed additional information to handle sequences of commands and the while command, to be supplied by the user. This paper explores the alternative approach described but not investigated by Gordon. It yields great expressiveness and control in stating and proving as theorems within HOL concepts which previously were only describable as meta-theorems outside HOL. For example, we have proven the assignment axiom described above: ` 8q x e: fq [x := e]g x := e fqg where q [x := e] is a substituted version of q, described later. To achieve this expressiveness, it is necessary to create a deeper foundation than that used previously. Instead of using an extension of the HOL Object Language as the programming language, we create an entirely new set of datatypes within the Object Language to represent constructs of the programming language and the associated assertion language. This is known as a \deep" embedding, as opposed to the shallow embedding developed by Gordon. This allows a significant dierence in the way that the semantics of the programming language is dened. Instead of dening a construct as its semantic meaning, we dene the construct as simply a syntactic constructor of phrases in the programming language, and then separately dene the semantics of each construct in a structural operational semantics [Winskel 93]. This separation means that we can now decompose and analyze syntactic program phrases at the HOL Object Language level, and thus reason within HOL about the semantics of purely syntactic manipulations, such as substitution or verication condition generation, since they exist within the HOL logic. This has denite advantages because syntactic manipulations, when semantically correct, are simpler and easier to calculate. They encapsulate a level of detailed semantic reasoning that then only needs to be proven once, instead of having to be repeatedly proven for every occurrence of that manipulation. This will be a recurring pattern in this paper, where repeatedly a syntactic manipulation is dened, and then its semantics is described and proven correct within HOL. 3. HIGHER ORDER LOGIC Higher Order Logic (HOL) [Gordon 93] is a version of predicate calculus that allows variables to range over functions and predicates. Thus denotable values may be functions of any higher order. Strong typing ensures the consistency and proper meaning of all expressions. The power of this logic is similar to set theory, and it is sucient for expressing most mathematical theories. HOL is also a mechanical proof development system. It is secure in that only true theorems can be proved. Rather than attempting to automatically prove theorems, HOL acts as a supportive assistant, mechanically checking the validity of each step attempted by the user. It provides tools to dene within the logic new types and constants, including primitive recursive functions, functions specied by properties, and relations dened by rule induction.
3 A Mechanically Verified Verification Condition Generator 3 The primary interface to HOL is the polymorphic functional programming language ML (\Meta Language") [Cousineau 86]; commands to HOL are expressions in ML. Within ML is a second language OL (\Object Language"), representing terms and theorems by ML abstract datatypes term and thm. A shallow embedding represents program constructs by new OL functions to combine the semantics of the constituents to produce the semantics of the combination. Our approach is to dene a third level of language, contained within OL as concrete recursive datatypes, to represent the constructs of the programming language PL being studied and its associated assertion language AL. We begin with the denition of variables. 4. VARIABLES AND VARIANTS A variable is represented by a new concrete type var, with one constructor, VAR:string->num->var. We dene two deconstructor functions, Base (VAR str n) = str and Index (VAR str n) = n. The number attribute eases the creation of variants of a variable, which are made by (possibly) increasing the number. All possible variables are considered predeclared of type num (nonnegative integers). In future versions, we hope to treat other data types. Some languages distinguish between program variables and logical variables, which cannot be changed by program control. In this simple language, this is unnecessary. Our recent work with procedure calls supports logical variables. The variant function has type var->(var)set->var. variant x s returns a variable which is a variant of x, which is guaranteed not to be in the \exclusion" set s. If x is not in the set s, then it is its own variant. This is used in dening proper substitution on quantied expressions. The denition of variant is somewhat deeper than it might originally appear. To have a constructive function for making variants in particular instances, we wanted () variant x s = (x 2 s => variant (mk variant x 1) s x) where mk variant (VAR str n) k = VAR str (n + k). For any nite set s, this denition of variant will terminate, but unfortunately, it is not primitive recursive. As a substitute, we wanted to dene the variant function by specifying its properties, as 1) (variant x s) is variant x ; 2) (variant x s 2 s) ; 3) 8z: if (z is variant x) ^ (z 2 s) then Index (variant x s) Index z, where we dene y is variant x = (Base y = Base x ^ Index x Index y) : But the above specication did not easily support the proof of the existence theorem, that such a variant existed for any x and s, because the set of values for z satisfying the third property's antecedent is innite; we work strictly with nite sets. The solution was to introduce the function variant set, where variant set x n returns the set of the rst n variants of x, all dierent from each other, so CARD (variant set x n) = n. Its denition is variant set x 0 = f g ; variant set x (n + 1) = fmk variant x ng [ (variant set x n) : Then by the pigeonhole principle, we are guaranteed that variant set x ((CARD s) + 1) must contain at least one variable which is not in the set s. This leads to the needed existence theorem. We then dened variant with properties 1 0 ) (variant x s) 2 variant set x ((CARD s) + 1) ; 2 0 ) (variant x s 2 s) ; 3 0 ) 8z: if z 2 variant set x ((CARD s) + 1) ^ (z 2 s) then Index (variant x s) Index z : From this denition, we then proved both the original set of properties (1)-(3), and also the constructive function denition () given above, as theorems. 5. PROGRAMMING AND ASSERTION LANGUAGES The syntax of the programming language PL is exp: e ::= n j x j ++ x j e 1 + e 2 j e 1 e 2 bexp: b ::= e 1 = e 2 j e 1 < e 2 j b 1 ^ b 2 j b 1 _ b 2 j b cmd: c ::= skip j abort j x := e j c 1 ; c 2 j if b then c 1 else c 2 j assert a while b do c Table 1: Programming Language Syntax Most of these constructs are standard. n is an unsigned integer; x is a variable; ++ is the increment operator; abort causes an immediate abnormal termination; the while loop requires an invariant assertion to be supplied. The notation used above is for ease of reading; each phrase is actually formed by a constructor function, e.g., ASSIGN:var->exp->cmd for assignment. The syntax of the associated assertion language AL is vexp: v ::= n j x j v 1 + v 2 j v 1 v 2 j v 1 v 2 aexp: a ::= true j false j v 1 = v 2 j v 1 < v 2 j a 1 ^ a 2 j a 1 _ a 2 j a j a 1 ) a 2 j a 1 = a 2 j a 1 => a 2 a 3 j close a j 8x: a j 9x: a Table 2: Assertion Language Syntax Again, most of these expressions are standard. a 1 => a 2 a 3 is a conditional expression, yielding the
4 4 Peter V. Homeier and David F. Martin value of a 2 or a 3 depending on the value of a 1. close a forms the universal closure of a, which is true when a is true for all possible assignments to its free variables. The constructor function AVAR:var->vexp creates a vexp from a variable. We overload the same operator in dierent languages, asking the reader to disambiguate by context. 6. OPERATIONAL SEMANTICS The semantics of the programming language is expressed by the following three relations. The values of all variables are in num so a state is represented by a mapping from variables to num. E e s 1 n s 2 : B b s 1 t s 2 : numeric expression e:exp evaluated in state s 1 yields numeric value n:num and state s 2 : boolean expression b:bexp evaluated in state s 1 yields truth value t:bool and state s 2 : C c s 1 s 2 : command c:cmd evaluated in state s 1 yields state s 2 : Table 3 gives the structural operational semantics [Winskel 93] of the programming language PL, given as rules inductively dening the three relations E, B, and C. These relations are dened within HOL using Tom Melham's excellent rule induction package [Camilleri 92,Melham 92]. The notation s[v=x] indicates the state s updated so that (s[v=x])(x) = v. This denition is straightforward, and is easy to read and analyze once the notation is understood. Table 4 gives the semantics of the assertion language AL by recursive functions dened on the structure of the construct, in a directly denotational fashion. V v s : A a s : numeric expression v:vexp evaluated in state s yields a numeric value in num : boolean expression a:aexp evaluated in state s yields a truth value in bool : 7. SUBSTITUTION We dene proper substitution on assertion language expressions using the technique of simultaneous substitutions, following Stoughton [Stoughton 88]. The usual denition of proper substitution is a fully recursive function. Unfortunately, HOL only supports primitive recursive denitions. To overcome this, we use simultaneous substitutions, which are represented by functions of type subst = var->vexp. This describes a family of substitutions, all of which are considered to take place simultaneously. This family is in principle innite, but in practice all but a nite number of the substitutions are the identity substitution. The virtue of this approach is that the application of a simultaneous substitution to an assertion language expression may be dened using only primitive recursion, not full recursion, and then the normal single substitution operation of [v=x] may be dened as a special case: [v=x] = y: (y = x => v AVAR y) : We apply a substitution by the inx operator. Thus, a ss denotes the application of the simultaneous substitution ss to the expression a, where a can be either vexp or aexp. Therefore a [v=x] denotes the single substitution of the expression v for the variable x wherever x appears free in a. Finally, there is a dual notion of applying a simultaneous substitution to a state, instead of to an expression; this is called semantic substitution, and is dened as s ss = y: (V (ss y) s). Most of the cases of the denition of the application of a substitution to an expression are simply the distribution of the substitution across the immediate subexpressions. The interesting cases of the denition of a ss are where a is a quantied expression, for example: (8x: S a) ss = let free = z2(f Va a) fxg F V v (ss z) in let y = variant x free in 8y: (a (ss[(avar y) = x])) : Here F V a and F V v are functions that return the set of free variables in an aexp or vexp expression, and variant x free is a function that yields a new variable as a variant of x, guaranteed not to be in the set free. Once we have dened substitution as a syntactic manipulation, we can then prove the following two theorems about the semantics of substitution: ` 8v s ss: V (v ss) s = V v (s ss) ` 8a s ss: A (a ss) s = A a (s ss) : This is our statement of the Substitution Lemma of logic, and essentially says that syntactic substitution is equivalent to semantic substitution. 8. TRANSLATION Expressions have typically not been treated in previous work on verication; there are some exceptions, notably Sokolowski [Sokolowski 84]. Expressions with side effects have been particularly excluded. Since expressions did not have side eects, they were often considered to be a sublanguage, common to both the programming language and the assertion language. Thus one would commonly see expressions such as p ^ b, where p was an assertion and b was a boolean expression from the programming language. One of the key realizations of this work was the need to carefully distinguish these two languages, and not confuse their expression sublanguages. This then requires us to translate programming language expressions into the assertion language before the two may be combined as above. In fact, since we allow expressions to have side eects, there are actually two results of translating a programming language expression e:
5 A Mechanically Verified Verification Condition Generator 5 Number : Variable : Increment : E x s 1 n s 2 E (n) s n s E (x) s s(x) s E (++ x) s 1 (n + 1) s 2 [(n + 1)=x] E Addition : Subtraction : E e 1 s 1 n 1 s 2 ; E e 2 s 2 n 2 s 3 E (e 1 + e 2 ) s 1 (n 1 + n 2 ) s 3 E e 1 s 1 n 1 s 2 ; E e 2 s 2 n 2 s 3 E (e 1 e 2 ) s 1 (n 1 n 2 ) s 3 Equality : Less Than: B E e 1 s 1 n 1 s 2 ; E e 2 s 2 n 2 s 3 B (e 1 = e 2 ) s 1 (n 1 = n 2 ) s 3 E e 1 s 1 n 1 s 2 ; E e 2 s 2 n 2 s 3 E (e 1 < e 2 ) s 1 (n 1 < n 2 ) s 3 Conjunction : Disjunction : Negation : B b 1 s 1 t 1 s 2 ; B b 2 s 2 t 2 s 3 B (b 1 ^ b 2 ) s 1 (t 1 ^ t 2 ) s 3 B b 1 s 1 t 1 s 2 ; B b 2 s 2 t 2 s 3 B (b 1 _ b 2 ) s 1 (t 1 _ t 2 ) s 3 B b s 1 t s 2 B ( b) s 1 ( t) s 2 Skip : Conditional : C skip s s Abort : (no rules) B b s 1 T s 2 ; C c 1 s 2 s 3 C (if b then c 1 else c 2 ) s 1 s 3 B b s 1 F s 2 ; C c 2 s 2 s 3 C (if b then c 1 else c 2 ) s 1 s 3 C Assignment : Iteration : E e s 1 n s 2 C (x := e) s 1 s 2 [n=x] B b s 1 T s 2 ; C c s 2 s 3 C (assert a while b do c) s 3 s 4 C (assert a while b do c) s 1 s 4 Sequence : C c 1 s 1 s 2 ; C c 2 s 2 s 3 C (c 1 ; c 2 ) s 1 s 3 B b s 1 F s 2 C (assert a while b do c) s 1 s 2 Table 3: Programming Language Structural Operational Semantics V V n s = n V x s = s(x) V (v 1 + v 2 ) s = (V v 1 s + V v 2 s) ( ; treated analogously) A true s = T A false s = F A (v 1 = v 2 ) s = (V v 1 s = V v 2 s) (< treated analogously) A A (a 1 ^ a 2 ) s = (A a 1 s ^ A a 2 s) (_; ; ); a 1 = a 2 ; a 1 => a 2 a 3 treated analogously) A (close a) s = (8s 1 : A a s 1 ) A (8x: a) s = (8n: A a s[n=x]) A (9x: a) s = (9n: A a s[n=x]) Table 4: Assertion Language Denotational Semantics
6 6 Peter V. Homeier and David F. Martin an assertion language expression, representing the value of e in the state \before" evaluation; a simultaneous substitution, representing the change in state from \before" evaluating e to \after" evaluating e. For example, the translator for numeric expressions is dened using a helper function VE 1: exp -> subst -> (aexp # subst) (where # denotes Cartesian product): VE1 (n) ss = n; ss (\," makes a pair) VE1 (x) ss = (ss x); ss VE1 (++ x) ss = (ss x) + 1; ss[((ss x) + 1) = x] VE1 (e 1 + e 2 ) ss = (VE1 e 1! v 1 : (VE1 e 2! v 2 ss 2 : (v 1 + v 2 ; ss 2 ))) ss VE1 (e 1 e 2 ) ss = (VE1 e 1! v 1 : (VE1 e 2! v 2 ss 2 : (v 1 v 2 ; ss 2 ))) ss where! is a \translator continuation" operator, de- ned as (f! k) ss = let (v; ss 0 ) = f ss in k v ss 0 : Then dene VE e = fst (VE1 e ) VE state e = snd (VE1 e ) where is the identity substitution and \fst" and \snd" select the elements of a pair. We can then prove that these translation functions, as syntactic manipulations, are semantically correct, according to the following theorem: ` 8e s 1 n s 2 : ((E e s 1 n s 2 ) = (n = V (VE e) s 1 ^ s 2 = s 1 (VE state e))) : Similar functions are used to translate boolean expressions. We dene the helper function AB1 and the main translation functions AB and AB state, and prove their correctness as ` 8b s 1 t s 2 : ((B b s 1 t s 2 ) = (t = A (AB b) s 1 ^ s 2 = s 1 (AB state b))) : These theorems mean that every evaluation of a programming language expression has its semantics completely captured by the two translation functions for its type. These are essentially small compiler correctness proofs. As a byproduct, we may now dene the simultaneous substitution that corresponds to an assignment statement, overriding the expression's state change with the change of the assignment: [x := e] = (VE state e)[(ve e) = x] : 9. AXIOMATIC SEMANTICS The semantics of Floyd/Hoare partial correctness formulae is dened in Table 5. Given these formulae, we can now express the axiomatic semantics of the programming language (Table 6), and prove each rule as a theorem from the previous structural operational semantics. The most interesting of these proofs was that of the while-loop rule. It was necessary to prove a subsidiary lemma rst, by the strong version of rule induction for command semantics provided by Tom Melham's rule induction package. Strong induction allowed as inductive hypotheses instances of the command semantic relation C for \lower levels" in the relation built up by rule induction, as well as inductive hypotheses that those tuples satised the lemma. Although we did prove analogous theorems as an axiomatic semantics for both the numeric and boolean expressions in the programming language, it turned out that there was a better way to handle them provided through the translation functions. Using these translation functions, we may dene functions to compute the appropriate precondition to an expression, given the postcondition, as ae pre e a = a (VE state e) ab pre b a = a (AB state b) We may now prove the condensed axiomatic semantics for expressions given in Table 7. These precondition functions now allow us to revise the rules of inference for conditionals and loops, as given in Table VERIFICATION CONDITION GENER- ATOR We now dene a verication condition generator for this programming language. To begin, we rst dene a helper function vcg1, of type cmd->aexp->(aexp # (aexp)list). This function takes a command and a postcondition, and returns a precondition and a list of verication conditions that must be proved in order to verify that command with respect to the precondition and postcondition. This function does most of the work of calculating verication conditions. vcg1 is called by the main verication condition generator function, vcg, with type aexp->cmd->aexp-> (aexp)list. vcg takes a precondition, a command, and a postcondition, and returns a list of the verication conditions for that command. vcg1 and vcg are dened in Table 9, in which [ ] denotes the empty list and ampersand (&) is an inx version of HOL's AP- PEND operator to join two lists. The correctness of the VCG functions dened in Table 9 is established by proving the following theorems from the axioms and rules of inference of the axiomatic semantics: VCG1 THM: ` 8c q: let (p; h) = vcg1 c q in (every close h ) fpg c fqg) VCG THM: ` 8p c q: every close (vcg p c q) ) fpg c fqg every P lst is dened in HOL as being true when for every element x in the list lst, the predicate P is true when applied to x. Accordingly, every close h means that the universal closure of every verication condition in h is true.
7 A Mechanically Verified Verification Condition Generator 7 aexp: fag = close a = 8s: A a s exp: fpg e fqg = 8n s 1 s 2 : A p s 1 ^ E e s 1 n s 2 ) A q s 2 bexp: fpg b fqg = 8t s 1 s 2 : A p s 1 ^ B b s 1 t s 2 ) A q s 2 cmd: fpg c fqg = 8s 1 s 2 : A p s 1 ^ C c s 1 s 2 ) A q s 2 Table 5: Floyd/Hoare Partial Correctness Semantics Skip : Abort : fqg skip fqg ffalseg abort fqg Assignment : Sequence : fq [x := e]g x := e fqg fpg c 1 frg; frg c 2 fqg fpg c 1 ; c 2 fqg Conditional : Iteration : fp ^ AB(b)g b fr 1 g fp ^ AB(b)g b fr 2 g fr 1 g c 1 fqg; fr 2 g c 2 fqg fpg if b then c 1 else c 2 fqg fa ^ AB(b)g b fpg fa ^ AB(b)g b fqg fpg c fag fag assert a while b do c fqg Table 6: Programming Language Axiomatic Semantics Numeric expression precondition: fae pre e qg e fqg Boolean expression precondition: fab pre b qg b fqg Table 7: Programming Language Expression Axiomatic Semantics Conditional : Iteration : fr 1 g c 1 fqg; fr 2 g c 2 fqg fab b => ab pre b r 1 ab pre b r 2 g if b then c 1 else c 2 fqg fa ^ AB(b) ) ab pre b pg fa ^ AB(b) ) ab pre b qg fpg c fag fag assert a while b do c fqg Table 8: Programming Language Axiomatic Semantics (revisions)
8 8 Peter V. Homeier and David F. Martin vcg1 (skip) q = q; [ ] vcg1 (abort) q = true; [ ] vcg1 (x := e) q = q [x := e]; [ ] vcg1 (c 1 ; c 2 ) q = let (r; h 2 ) = vcg1 c 2 q in let (p; h 1 ) = vcg1 c 1 r in p; (h 1 & h 2 ) vcg1 vcg1 (if b then c 1 else c 2 ) q = let (r 1 ; h 1 ) = vcg1 c 1 q in let (r 2 ; h 2 ) = vcg1 c 2 q in (AB b => ab pre b r 1 ab pre b r 2 ); (h 1 & h 2 ) vcg1 (assert a while b do c) q = let (p; h) = vcg1 c a in a; [a ^ AB b ) ab pre b p ; a ^ (AB b) ) ab pre b q] & h vcg vcg p c q = let (r; h) = vcg1 c q in [p ) r] & h Table 9: Verication Condition Generator These theorems are proven from the axiomatic semantics by induction on the structure of the command involved. This veries the VCG. It shows that the vcg function is sound, that the correctness of the verication conditions it produces suce to establish the correctness of the annotated program. This does not show that the vcg function is complete, that if a program is correct, then the vcg function will produce a set of verication conditions sucient to prove the program correct from the axiomatic semantics [Cook 78]. However, this soundness result is quite useful, in that we may directly apply these theorems in order to prove individual programs partially correct within HOL, as seen in the next section. 11. EXAMPLE PROGRAMS Given the vcg function dened in the last section and its associated correctness theorem, proofs of program correctness may now be partially automated with security. This has been implemented in an HOL tactic, called VCG TAC, which transforms a given program correctness goal to be proved into a set of subgoals which are the verication conditions returned by the vcg function. These subgoals are then proved within the HOL theorem proving system, using all the power and resources of that theorem prover, directed by the user's ingenuity. As an example, we will take the quotient/remainder algorithm for integer division by repeated subtraction. The program to be veried, with the annotations of the loop invariant and pre- and postconditions, is shown in Table 10. Since x0 and y0 do not appear in the program text, their values cannot be altered by the program. This specication means that if the program terminates, the nal value of q must be the quotient of the division of x0 by y0, and r the remainder. A transcript of the application of VCG TAC to this problem is shown in Table 11. We have written a parser for the subject language, using the parser library in HOL, invoked using the delimiters \[[" and \]]". The partial correctness goal is parsed and converted into the abstract syntax form used internally. VCG TAC then converts that goal into verication conditions in the Object Language of HOL. These verication conditions are now each solved as a subgoal by normal HOL theorem proving techniques. The Object Language variables involved in these verication conditions are constructed to have names similar to the original program variable names; if there is a non-zero variant number, it is appended to the variable name. Thus, if program variable x were changed to z in the example of Table 11, the verication conditions would be the same but with the OL variable z in place of x. The VCG TAC tactic rst applies the theorem VCG THM to reason backwards from the program correctness statement to a goal invoking the vcg function. By the theorem, the proof of these verication conditions will establish the proof of the original program correctness statement. The next step of VCG TAC is to \execute" the various syntactic manipulation functions mentioned in the current goal by symbolically rewriting the goal using the denitions of the functions, including vcg, vcg1, translations, substitutions, and substitution application. Be-
9 A Mechanically Verified Verification Condition Generator 9 fx0 = x ^ y0 = yg r := x ; q := 0 ; assert x0 = q y0 + r ^ y0 = y while (r < y) do r := r y ; q := ++ q od fx0 = q y0 + r ^ r < y0g Table 10: Quotient/Remainder Algorithm #g [[ fx0 = x /\ y0 = yg # r := x; # q := 0; # assert x0 = q * y0 + r /\ y0 = y # while (r < y) do # r := r - y; # q := ++q # od # fx0 = q * y0 + r /\ r < y0g # ]];;... #e(vcg TAC);; OK.. 3 subgoals "!x0 q y0 r y. ((x0 = (q * y0) + r) /\ (y0 = y)) /\ r < y ==> (x0 = (q * y0) + r) /\ r < y0" "!x0 q y0 r y. ((x0 = (q * y0) + r) /\ (y0 = y)) /\ r < y ==> (x0 = ((q + 1) * y0) + (r - y)) /\ (y0 = y)" "!x0 x y0 y. (x0 = x) /\ (y0 = y) ==> (x0 = (0 * y0) + x) /\ (y0 = y)" () : void Run time: 80.3s Intermediate theorems generated: 5643 Table 11: Transcript of Application of VGC TAC to Q/R Algorithm
10 10 Peter V. Homeier and David F. Martin cause the rewriting process is done symbolically, instead of actually executing a program, it is relatively slow, but complete soundness is assured. This \execution" converts the invocation of the vcg function on the annotated program into the actual set of verication conditions that the vcg function returns. Afterwards, the goal is left as a set of \constant" verication conditions in the assertion language. VCG TAC then uses the denitions of the semantics of the assertion language to rewrite these verication conditions into equivalent statements in the Object Language of HOL, using the denitions of close, A, and V. In particular, all references to assertion language variables within program states are converted to references to similarly-named OL variables. These verication conditions are then presented to the user as the necessary subgoals that need to be solved in order to complete the proof of the program originally presented. 12. FUTURE WORK We are currently extending this work to include several more language features, principally mutually recursive procedures and concurrency. In addition, we are working on VCGs for total correctness. We have completed the extension of the work reported in this paper to include total correctness, using the same semantic specication style and requiring additions to the invariant assertions for while loops. Work on mutually recursive procedures requires many new concepts and techniques to dene the semantics and perform verication condition generator proofs. These include declarations of procedures, their collection into environments, their verication independent of actual use of the procedures, well-formedness conditions on programs, and the delicate issue of parameter passing. We have completed, in HOL, a mechanized proof of correctness of a partial correctness VCG for a language that includes mutually recursive procedures. This work used the semantic specication style of this paper, and required suitable assertions in procedure headings. Work is proceeding toward formulating and mechanically verifying a total correctness VCG for the same language. In future versions we hope to treat other datatypes by embedding a type system within our programming language, and by introducing a more complex state and a static semantics for the language which performs typechecking. This would use HOL's built-in datatypes to support booleans, strings, lists, etc. Concurrency raises a whole host of new issues, ranging from the level of structural operational semantics (\big-step" versus \small-step"), to dealing with assertions describing temporal sequences of states instead of single states, to issues of fairness. We believe that a proper treatment of concurrency will exhibit qualities of modularity and compositionality. Modularity means that a specication for a process should state both (a) the assumptions under which it should operate, and (b) the task (or commitment) which it should meet, given those assumptions. Compositionality means that the specication of a system of processes should be veri- able in terms of the specications of the individual constituent processes. 13. SUMMARY AND CONCLUSIONS The fundamental contribution of this work is the exhibition of a tool to ease the task of proving programs which is itself proven to be sound. This verication condition generator tool performs an automatic, syntactic transformation of the annotated program into a set of verication conditions. The verication conditions produced are themselves proven within HOL, establishing the correctness of the program within the same system wherein the VCG was veried. This proof of the correctness of the VCG may be considered as an instance of a compiler correctness proof, with the VCG translating from annotated programs to lists of verication conditions. Each of these has its semantics dened, and the VCG correctness theorem closes the commutative diagram, showing that the truth of the verication conditions implies the truth of the annotated program. The programming language and its associated assertion language are represented by new concrete recursive datatypes. This implies that they are completely independent of other data types and operations existing in the HOL system, without any hidden associations that might aect the validity of proof. This requires substantial work in dening their semantics and in proving the axioms and rules of inference of the axiomatic semantics from the operational semantics. However, this deeply embedded approach yields great expressiveness, ductility, and the ability to prove as theorems within HOL the correctness of various syntactic manipulations, which could only be stated as meta-theorems before. These theorems encapsulate a level of reasoning which now does not need to be repeated every time a program is veried, raising the level of proof from the semantic level to the syntactic. But the most important part of this work is the degree of trustworthiness of this syntactic reasoning. Verication condition generators are not new, but we are not aware of any other proofs of their correctness to this level of rigor. This enables program proofs which are both trustworthy and eective. REFERENCES Agerholm 92: S. Agerholm, Mechanizing Program Verication in HOL. In Proc. of the 1991 International Workshop on the HOL Theorem Proving System and its Applications, pp. 208{222, M. Archer, J. J. Joyce, K. N. Levitt, and P. J. Windley (eds.), IEEE Computer Society Press (1992). Camilleri 92: J. Camilleri and T. Melham, Reasoning with Inductively Dened Relations in the HOL Theorem
11 A Mechanically Verified Verification Condition Generator 11 Prover. Technical Report No. 265, University of Cambridge Computer Laboratory, (1992). Cook 78: S. A. Cook, Soundness and Completeness of an Axiom System for Program Verication. SIAM Journal on Computing, 7, pp. 70{90, (1978). Cousineau 86: G. Cousineau, M. Gordon, G. Huet, R. Milner, L. Paulson, and C. Wadsworth, The ML Handbook, INRIA (1986). Gordon 89: M. J. C. Gordon, Mechanizing Programming Logics in Higher Order Logic. In Current Trends in Hardware Verication and Automated Theorem Proving, pp. 387{489, P. A. Subrahmanyam and G. Birtwistle (eds.), Springer-Verlag, New York (1989). Gordon 93: M. J. C. Gordon and T. F. Melham, Introduction to HOL, Cambridge University Press, Cambridge (1993). Igarashi 75: S. Igarashi, R. L. London, and D. C. Luckham, Automatic Program Verication I: A Logical Basis and its Implementation. ACTA Informatica, 4, pp. 145{182 (1975). Melham 92: T. Melham, A Package for Inductive Relation Denitions in HOL. In Proc. of the 1991 International Workshop on the HOL Theorem Proving System and its Applications, pp. 350{357, M. Archer, J. J. Joyce, K. N. Levitt, and P. J. Windley (eds.), IEEE Computer Society Press (1992). Ragland 73: L. C. Ragland, A Veried Program Verier. Technical Report No. 18, Department of Computer Sciences, University of Texas at Austin (1973). Sokolowski 84: S. Sokolowski, Partial Correctness: The Term-Wise Approach. Science of Computer Programming, 4, pp. 141{157 (1984). Stoughton 88: A. Stoughton, Substitution Revisited. Theoretical Computer Science, 59, pp. 317{325, (1988). Winskel 93: G. Winskel, The Formal Semantics of Programming Languages, An Introduction. The MIT Press, Cambridge, (1993).
Abstract. The verication of programs that contain mutually recursive. to be unsound. Verication Condition Generator (VCG) tools
Mechanical Verication of Mutually Recursive Procedures Peter V. Homeier and David F. Martin UCLA Computer Science Department Los Angeles, California 924 USA firstname.lastname@example.com and email@example.com 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: email@example.com Phone: +81 94 38 5130More 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
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
International Journal of Computer ScienceandCommunication Vol. 2, No. 1, January-June2011, pp. 153-157 PROPERTECHNIQUEOFSOFTWARE INSPECTIONUSING GUARDED COMMANDLANGUAGE Neeraj Kumar Singhania University,More information
University of California. Los Angeles. Trustworthy Tools for Trustworthy Programs: A Mechanically Veried. of the requirements for the degree
University of California Los Angeles Trustworthy Tools for Trustworthy Programs: A Mechanically Veried Verication Condition Generator for the Total Correctness of Procedures A dissertation submitted inMore 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
Pretty-big-step semantics
Pretty-big-step semantics Arthur Charguéraud INRIA October 2012 1 / 34 Motivation Formalization of JavaScript with Sergio Maeis, Daniele Filaretti, Alan Schmitt, Martin Bodin. Previous work: Semi-formalMore 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
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
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
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
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
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
Functional Programming. Functional Programming Languages. Chapter 14. Introduction
Functional Programming Languages Chapter 14 Introduction Functional programming paradigm History Features and concepts Examples: Lisp ML 1 2 Functional Programming Functional Programming Languages TheMore 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
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
Language. Johann Eder. Universitat Klagenfurt. Institut fur Informatik. Universiatsstr. 65. A-9020 Klagenfurt / AUSTRIA
PLOP: A Polymorphic Logic Database Programming Language Johann Eder Universitat Klagenfurt Institut fur Informatik Universiatsstr. 65 A-9020 Klagenfurt / AUSTRIA February 12, 1993 Extended Abstract TheMore information
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
Rigorous Software Engineering Hoare Logic and Design by Contracts
Rigorous Software Engineering Hoare Logic and Design by Contracts Simão Melo de Sousa RELEASE (UBI), LIACC (Porto) Computer Science Department University of Beira Interior, Portugal 2010-2011 S. Melo deMore 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
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: firstname.lastname@example.com 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
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
A Propositional Dynamic Logic for CCS Programs
A Propositional Dynamic Logic for CCS Programs Mario R. F. Benevides and L. Menasché Schechter {mario,email@example.com Abstract This work presents a Propositional Dynamic Logic in which the programs areMore information
Constructing Contracts: Making Discrete Mathematics Relevant to Beginning Programmers
Constructing Contracts: Making Discrete Mathematics Relevant to Beginning Programmers TIMOTHY S. GEGG-HARRISON Winona State University Although computer scientists understand the importance of discreteMore information
Formal Verification Coverage: Computing the Coverage Gap between Temporal Specifications
Formal Verification Coverage: Computing the Coverage Gap between Temporal Specifications Sayantan Das Prasenjit Basu Ansuman Banerjee Pallab Dasgupta P.P. Chakrabarti Department of Computer Science & EngineeringMore 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
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
Static Program Transformations for Efficient Software Model Checking
Static Program Transformations for Efficient Software Model Checking Shobha Vasudevan Jacob Abraham The University of Texas at Austin Dependable Systems Large and complex systems Software faults are majorMore 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
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
Introduction to formal semantics -
Introduction to formal semantics - Introduction to formal semantics 1 / 25 structure Motivation - Philosophy paradox antinomy division in object und Meta language Semiotics syntax semantics PragmaticsMore 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
Chapter 7: Functional Programming Languages
Chapter 7: Functional Programming Languages Aarne Ranta Slides for the book Implementing Programming Languages. An Introduction to Compilers and Interpreters, College Publications, 2012. Fun: a languageMore 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
Likewise, we have contradictions: formulas that can only be false, e.g. (p p).
CHAPTER 4. STATEMENT LOGIC 59 The rightmost column of this truth table contains instances of T and instances of F. Notice that there are no degrees of contingency. If both values are possible, the formulaMore 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
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
Chapter 2: Problem Solving Using C++
Chapter 2: Problem Solving Using C++ 1 Objectives In this chapter, you will learn about: Modular programs Programming style Data types Arithmetic operations Variables and declaration statements CommonMore information
Fundamental Computer Science Concepts Sequence TCSU CSCI SEQ A
Fundamental Computer Science Concepts Sequence TCSU CSCI SEQ A A. Description Introduction to the discipline of computer science; covers the material traditionally found in courses that introduce problemMore information
Software Testing & Analysis (F22ST3): Static Analysis Techniques 2. Andrew Ireland
Software Testing & Analysis (F22ST3) Static Analysis Techniques Andrew Ireland School of Mathematical and Computer Science Heriot-Watt University Edinburgh Software Testing & Analysis (F22ST3): StaticMore information
Chair of Software Engineering. Software Verification. Assertion Inference. Carlo A. Furia
Chair of Software Engineering Software Verification Assertion Inference Carlo A. Furia Proving Programs Automatically The Program Verification problem: Given: a program P and a specification S = [Pre,More information
Compiler Design. Type Checking
Compiler Design Type Checking Static Checking Token Stream Parser Abstract Syntax Tree Static Checker Decorated Abstract Syntax Tree Intermediate Code Generator Intermediate Code Static (Semantic) ChecksMore information
Object-Oriented Software Specification in Programming Language Design and Implementation
Object-Oriented Software Specification in Programming Language Design and Implementation Barrett R. Bryant and Viswanathan Vaidyanathan Department of Computer and Information Sciences University of AlabamaMore information
(LMCS, p. 317) V.1. First Order Logic. This is the most powerful, most expressive logic that we will examine.
(LMCS, p. 317) V.1 First Order Logic This is the most powerful, most expressive logic that we will examine. Our version of first-order logic will use the following symbols: variables connectives (,,,,More 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
Is Sometime Ever Better Than Alway?
Is Sometime Ever Better Than Alway? DAVID GRIES Cornell University The "intermittent assertion" method for proving programs correct is explained and compared with the conventional method. Simple conventionalMore 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
A Typing System for an Optimizing Multiple-Backend Tcl Compiler
The following paper was originally published in the Proceedings of the Fifth Annual Tcl/Tk Workshop Boston, Massachusetts, July 1997 A Typing System for an Optimizing Multiple-Backend Tcl Compiler ForestMore information
Formal Languages and Automata Theory - Regular Expressions and Finite Automata -
Formal Languages and Automata Theory - Regular Expressions and Finite Automata - Samarjit Chakraborty Computer Engineering and Networks Laboratory Swiss Federal Institute of Technology (ETH) Zürich MarchMore information
Problems Encountered in the Machine-assisted Proof of Hardware? Paul Curzon University of Cambridge Computer Laboratory, Pembroke Street, Cambridge, UK. Email: firstname.lastname@example.com URL http://www.cl.cam.ac.uk/users/pc/More information
Cedalion A Language Oriented Programming Language (Extended Abstract)
Cedalion A Language Oriented Programming Language (Extended Abstract) David H. Lorenz Boaz Rosenan The Open University of Israel Abstract Implementations of language oriented programming (LOP) are typicallyMore information
Elementary Number Theory and Methods of Proof. CSE 215, Foundations of Computer Science Stony Brook University http://www.cs.stonybrook.
Elementary Number Theory and Methods of Proof CSE 215, Foundations of Computer Science Stony Brook University http://www.cs.stonybrook.edu/~cse215 1 Number theory Properties: 2 Properties of integers (wholeMore information
Software Quality Factors OOA, OOD, and OOP Object-oriented techniques enhance key external and internal software quality factors, e.g., 1. External (v
Object-Oriented Design and Programming Deja Vu? In the past: Structured = Good Overview of Object-Oriented Design Principles and Techniques Today: Object-Oriented = Good e.g., Douglas C. Schmidt www.cs.wustl.edu/schmidt/More 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
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
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
CS510 Software Engineering
CS510 Software Engineering Propositional Logic Asst. Prof. Mathias Payer Department of Computer Science Purdue University TA: Scott A. Carr Slides inspired by Xiangyu Zhang http://nebelwelt.net/teaching/15-cs510-seMore information
We will learn the Python programming language. Why? Because it is easy to learn and many people write programs in Python so we can share.
LING115 Lecture Note Session #4 Python (1) 1. Introduction As we have seen in previous sessions, we can use Linux shell commands to do simple text processing. We now know, for example, how to count words.More 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
OPERATIONAL TYPE THEORY by Adam Petcher Prepared under the direction of Professor Aaron Stump A thesis presented to the School of Engineering of
WASHINGTON NIVERSITY SCHOOL OF ENGINEERING AND APPLIED SCIENCE DEPARTMENT OF COMPTER SCIENCE AND ENGINEERING DECIDING JOINABILITY MODLO GROND EQATIONS IN OPERATIONAL TYPE THEORY by Adam Petcher PreparedMore information
Computer-Assisted Theorem Proving for Assuring the Correct Operation of Software
1 Computer-Assisted Theorem Proving for Assuring the Correct Operation of Software Amy Felty University of Ottawa Introduction to CSI5110 2 The General Problem From Evan I. Schwartz, Trust Me, I m YourMore 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
Invertible elements in associates and semigroups. 1
Quasigroups and Related Systems 5 (1998), 53 68 Invertible elements in associates and semigroups. 1 Fedir Sokhatsky Abstract Some invertibility criteria of an element in associates, in particular in n-aryMore information
CHAPTER 2. Logic. 1. Logic Definitions. Notation: Variables are used to represent propositions. The most common variables used are p, q, and r.
CHAPTER 2 Logic 1. Logic Definitions 1.1. Propositions. Definition 1.1.1. A proposition is a declarative sentence that is either true (denoted either T or 1) or false (denoted either F or 0). Notation:More information
CST.98.5.1 COMPUTER SCIENCE TRIPOS Part IB Wednesday 3 June 1998 1.30 to 4.30 Paper 5 Answer five questions. No more than two questions from any one section are to be answered. Submit the answers in fiveMore 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
Ensuring Consistency in Long Running Transactions
Ensuring Consistency in Long Running Transactions UCLA Computer Science Dept. Technical Report TR-070011 Jeffrey Fischer Rupak Majumdar Department of Computer Science, University of California, Los AngelesMore information
1 Operational Semantics for While
Models of Computation, 2010 1 1 Operational Semantics for While The language While of simple while programs has a grammar consisting of three syntactic categories: numeric expressions, which representMore information
1 Introduction. 2 An Interpreter. 2.1 Handling Source Code
1 Introduction The purpose of this assignment is to write an interpreter for a small subset of the Lisp programming language. The interpreter should be able to perform simple arithmetic and comparisonsMore information
Cartesian Products and Relations
Cartesian Products and Relations Definition (Cartesian product) If A and B are sets, the Cartesian product of A and B is the set A B = {(a, b) :(a A) and (b B)}. The following points are worth specialMore information
A Framework for the Semantics of Behavioral Contracts
A Framework for the Semantics of Behavioral Contracts Ashley McNeile Metamaxim Ltd, 48 Brunswick Gardens, London W8 4AN, UK email@example.com Abstract. Contracts have proved a powerful conceptMore information
Introduction to Proofs
Chapter 1 Introduction to Proofs 1.1 Preview of Proof This section previews many of the key ideas of proof and cites [in brackets] the sections where they are discussed thoroughly. All of these ideas areMore information
Revised Version of Chapter 23. We learned long ago how to solve linear congruences. ax c (mod m)
Chapter 23 Squares Modulo p Revised Version of Chapter 23 We learned long ago how to solve linear congruences ax c (mod m) (see Chapter 8). It s now time to take the plunge and move on to quadratic equations.More information
Automated Program Behavior Analysis
Automated Program Behavior Analysis Stacy Prowell firstname.lastname@example.com March 2005 SQRL / SEI Motivation: Semantics Development: Most engineering designs are subjected to extensive analysis; software isMore information
Verifying Semantic of System Composition for an Aspect-Oriented Approach
2012 International Conference on System Engineering and Modeling (ICSEM 2012) IPCSIT vol. 34 (2012) (2012) IACSIT Press, Singapore Verifying Semantic of System Composition for an Aspect-Oriented ApproachMore information
Indiana State Core Curriculum Standards updated 2009 Algebra I
Indiana State Core Curriculum Standards updated 2009 Algebra I Strand Description Boardworks High School Algebra presentations Operations With Real Numbers Linear Equations and A1.1 Students simplify andMore information
Midlands Graduate School in the Foundations of Computer Science
Midlands Graduate chool in the Foundations of omputer cience Operational emantics, Abstract Machines, and orrectness Roy L. role University of Leicester, 8th to 12th April 2006 University of Nottingham,More information
Software Verification and Testing. Lecture Notes: Z I
Software Verification and Testing Lecture Notes: Z I Motivation so far: we have seen that properties of software systems can be specified using first-order logic, set theory and the relational calculusMore information
Combinatorial PCPs with ecient veriers
Combinatorial PCPs with ecient veriers Or Meir Abstract The PCP theorem asserts the existence of proofs that can be veried by a verier that reads only a very small part of the proof. The theorem was originallyMore information
1.1 Related work For non-preemptive scheduling on uniformly related machines the rst algorithm with a constant competitive ratio was given by Aspnes e
A Lower Bound for On-Line Scheduling on Uniformly Related Machines Leah Epstein Jir Sgall September 23, 1999 firstname.lastname@example.com, Department of Computer Science, Tel-Aviv University, Israel; firstname.lastname@example.com,More information
Lecture Notes on Linear Search
Lecture Notes on Linear Search 15-122: Principles of Imperative Computation Frank Pfenning Lecture 5 January 29, 2013 1 Introduction One of the fundamental and recurring problems in computer science isMore information
6.045: Automata, Computability, and Complexity Or, Great Ideas in Theoretical Computer Science Spring, 2010. Class 4 Nancy Lynch
6.045: Automata, Computability, and Complexity Or, Great Ideas in Theoretical Computer Science Spring, 2010 Class 4 Nancy Lynch Today Two more models of computation: Nondeterministic Finite Automata (NFAs)More 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
It all depends on independence
Working Papers Institute of Mathematical Economics 412 January 2009 It all depends on independence Daniel Eckert and Frederik Herzberg IMW Bielefeld University Postfach 100131 33501 Bielefeld Germany email:More information
Validated Templates for Specification of Complex LTL Formulas
Validated Templates for Specification of Complex LTL Formulas Salamah Salamah Department of Electrical, computer, Software, and Systems Engineering Embry Riddle Aeronautical University 600 S. Clyde MorrisMore 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
From Workflow Design Patterns to Logical Specifications
AUTOMATYKA/ AUTOMATICS 2013 Vol. 17 No. 1 http://dx.doi.org/10.7494/automat.2013.17.1.59 Rados³aw Klimek* From Workflow Design Patterns to Logical Specifications 1. Introduction Formal methods in softwareMore information
The Student-Project Allocation Problem
The Student-Project Allocation Problem David J. Abraham, Robert W. Irving, and David F. Manlove Department of Computing Science, University of Glasgow, Glasgow G12 8QQ, UK Email: {dabraham,rwi,email@example.com information
Extended Static Checking for Java
Lukas TU München - Seminar Verification 14. Juli 2011 Outline 1 Motivation 2 ESC/Java example 3 ESC/JAVA architecture VC generator Simplify 4 JML + ESC/Java annotation language JML What ESC/Java checksMore 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
Rigorous. Development. Software. Program Verification. & Springer. An Introduction to. Jorge Sousa Pinto. Jose Bacelar Almeida Maria Joao Frade
Jose Bacelar Almeida Maria Joao Frade Jorge Sousa Pinto Simao Melo de Sousa Rigorous Software Development An Introduction to Program Verification & Springer Contents 1 Introduction 1 1.1 A Formal ApproachMore information
Using Patterns and Composite Propositions to Automate the Generation of Complex LTL
University of Texas at El Paso DigitalCommons@UTEP Departmental Technical Reports (CS) Department of Computer Science 8-1-2007 Using Patterns and Composite Propositions to Automate the Generation of ComplexMore information
CS 16: Assembly Language Programming for the IBM PC and Compatibles
CS 16: Assembly Language Programming for the IBM PC and Compatibles First, a little about you Your name Have you ever worked with/used/played with assembly language? If so, talk about it Why are you takingMore information
Glossary of Object Oriented Terms
Appendix E Glossary of Object Oriented Terms abstract class: A class primarily intended to define an instance, but can not be instantiated without additional methods. abstract data type: An abstractionMore information
Tool Support for Invariant Based Programming
Tool Support for Invariant Based Programming Ralph-Johan Back and Magnus Myreen Abo Akademi University, Department of Computer Science Lemminkainenkatu 14 A, FIN-20520 Turku, Finland Email: firstname.lastname@example.com,More information
A semantic approach to secure information ow
Science of Computer Programming 37 (2000) 113 138 www.elsevier.nl/locate/scico A semantic approach to secure information ow Rajeev Joshi a;, K. Rustan M. Leino b a Department of Computer Sciences, TheMore information
4 Domain Relational Calculus
4 Domain Relational Calculus We now present two relational calculi that we will compare to RA. First, what is the difference between an algebra and a calculus? The usual story is that the algebra RA isMore 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


text:
|Close Window
OYSTERS: Season set to open for 15 short days
Special to the Herald-Guide - May 17, 2007
Louisiana Department of Wildlife and Fisheries Secretary Bryant O. Hammett, Jr. announced a 15-day oyster season in the Little Lake Public area.
Oyster Seed Grounds and selected areas of the Vermilion/East and West Cote Blanche/Atchafalaya Bay Public Oyster Seed Grounds located east of South Point of Marsh Island and south of the Louisiana Department of Health and Hospitals' May to August 2007 seasonal reclassification line that generally runs from South Point of Marsh Island ENE to Point Chevreuil.
The short season in these areas will will close at one-half hour after sunset on Friday, May 18.
Much of the area within these public oyster seed grounds was previouslyclosed to harvest by the DHH seasonal reclassification lines during the 2006 - 2007-oyster season..
However, these areas will be open by the DHH May through August in the seasonal reclassification lines.
Substantial oyster resources continue to exist in these public oyster seed grounds in areas previously closed to harvest.
It has been determined by LDWF Marine Fisheries Division biologists that the reefs would benefit from limited harvest while providing economic opportunity to the oyster industry as it continues to rehabilitate from the hurricane impacts of 2005.
Read More Stories at HeraldGuide.com!
|heraldguide.com is a supplement to St. Charles Herald Guide.
Copyright © 2001 - 2017 St. Charles Herald Guide, Inc. All rights reserved.
Please contact our WebMaster if you experience problems with the website.


text:
Flagging concerns about fiscal and external imbalances in the economy, the apex bank said that more reforms are required, especially in road and power sectors, to remove the investment bottlenecks
Mumbai: The Reserve Bank of India (RBI) on Monday said recent reforms have reduced the immediate risks for the economy but emphasised on the need for more measures to restore investor confidence, reports PTI.
Flagging concerns about fiscal and external imbalances in the economy, the apex bank said that more reforms are required, especially in road and power sectors, to remove the investment bottlenecks.
"The fresh round of reforms that were initiated in September 2012, after a hiatus, has reduced the immediate risks facing the Indian economy...
"On the whole it appears that the reform measures taken so far have not decisively lifted business sentiments and further action may be needed to restore confidence," RBI said in its third quarter review of Macroeconomic and Monetary Development.
The monetary policy, RBI said, could focus more on boosting growth after the reform actions get executed.
"While government has embarked on a fiscal adjustment path, staying on this course over the medium-term is necessary for providing sufficient space for monetary policy to stimulate growth," RBI said.
In the past couple of months the government has taken a host of reforms initiative including opening the multi-brand retail chain to foreign direct investment (FDI), and also the Union Cabinet has approved hiking foreign investment limits in the insurance and pension sectors.
Earlier this month, the government also allowed partial deregulation of diesel prices, besides limiting the number of subsidised LPG cylinders to nine per family a year.
"Fiscal risks have somewhat moderated in 2012-13, but a sustained commitment to fiscal consolidation is needed to generate monetary space," RBI said.
Due to risks from high inflation and high current account and fiscal deficits the scope for supportive monetary policy action is constrained, says the central bank ahead of its third quarter monetary policy
Mumbai: Citing high inflation and widening current account deficit (CAD) as big constraints, the Reserve Bank of India (RBI) on Monday said there is limited scope for monetary actions like interest rate cut to boost growth in the third quarter policy to be announced on Tuesday, reports PTI.
"Given the preponderance of non-monetary factors behind the current slowdown in an environment where risks from high inflation, current account and fiscal deficits still remain, the scope for supportive monetary policy action is constrained", RBI said in its report on Macroeconomic and Monetary Developments issued on the eve of policy.
The central bank, however, said that with the government executing economic reforms measures, it would be possible for the monetary policy to increasingly focus on revival of growth.
Meanwhile, the professional forecasters sponsored by the RBI have lowered the growth projection for the current fiscal to 5.5% from 5.6% projected earlier. They have also cut the growth forecast for the next financial year to 6.5% from 6.6%.
As regards inflation, RBI said it was likely to moderate below its projection of 7.5% by March-end. However, it added, "suppressed inflation continues to pose a significant risk to the inflation in 2013-14. As some of the risks materialises, inflation path may turn stick."
Referring to recent reforms initiatives, it said, "(they) have reduced immediate risks, but there is a long road ahead to bring about a sustainable turnaround for the Indian economy. Business sentiments remain weak despite reform initiatives and consumer confidence is edging down."
During the all-party meeting convened by the Centre on Telangana in New Delhi on 28th December last year, Shinde had said the issue would be resolved within a month while Chidambaram, on 9 December 2009 had announced on initiating process to create Telangana state
Hyderabad: A local court on Monday directed police to investigate into the allegations whether Union ministers Sushilkumar Shinde and P Chidambaram 'cheated' the people of Telangana region by their statements on the statehood issue, reports PTI.
Based on a complaint filed by Telangana Junior Advocates' Association president Naresh Kumar, the Second Metropolitan Magistrate Court directed the LB Nagar police to investigate into the matter and file a status report before it by 14th February.
Kumar, in his petition, had mentioned about the statements of Shinde and Chidambaram on the Telangana issue and sought the court's directions to refer the matter to the police for investigation under section 420 (cheating) of the IPC.
During the all-party meeting convened by the Centre on Telangana in New Delhi on 28th December last year, home minister Sushilkumar Shinde had said the Telangana issue would be resolved within a month.
On 9 December 2009, the then Union home minister P Chidambaram had announced on initiating process to create Telangana state. However, on 23 December 2009 Chidambaram modified the statement following an agitation in coastal Andhra and Rayalseema regions of Andhra Pradesh.
Meanwhile, Cyberabad Police Commissioner Ch Dwaraka Tirumala Rao said they were yet to receive the court orders in this regard.
Asked if the police would lodge any case against the Union ministers, the senior police officer said, "We have to first go through the order copy and act accordingly."


text:
|Message view
|« Date » · « Thread »
|« Date » · « Thread »
|"Michael Busch (JIRA)" <j...@apache.org>
|[jira] Resolved: (LUCENE-761) Clone proxStream lazily in SegmentTermPositions
|Sun, 11 Mar 2007 07:16:09 GMT
[ https://issues.apache.org/jira/browse/LUCENE-761?page=com.atlassian.jira.plugin.system.issuetabpanels:all-tabpanel ] Michael Busch resolved LUCENE-761. ---------------------------------- Resolution: Fixed Fix Version/s: 2.2 I just committed this. > Clone proxStream lazily in SegmentTermPositions > ----------------------------------------------- > > Key: LUCENE-761 > URL: https://issues.apache.org/jira/browse/LUCENE-761 > Project: Lucene - Java > Issue Type: Improvement > Components: Index > Reporter: Michael Busch > Assigned To: Michael Busch > Priority: Minor > Fix For: 2.2 > > Attachments: lucene-761.patch > > > In SegmentTermPositions the proxStream should be cloned lazily, i. e. at the first time nextPosition() is called. Then the initialization costs of TermPositions are not higher anymore compared to TermDocs and thus there is no reason anymore for Scorers to use TermDocs instead of TermPositions. In fact, all Scorers should use TermPositions, because custom subclasses of existing scorers might want to access payloads, which is only possible via TermPositions. We could further merge SegmentTermDocs and SegmentTermPositions into one class and deprecate the interface TermDocs. > I'm going to attach a patch once the payloads feature (LUCENE-755) is committed. -- This message is automatically generated by JIRA. - You can reply to this email to add a comment to the issue online. --------------------------------------------------------------------- To unsubscribe, e-mail: firstname.lastname@example.com For additional commands, e-mail: email@example.com
|View raw message


text:
So this is what it's like to make a film "based on a true story." How Lifetime of us.
CSNNE.com Bruins Insider Joe Haggerty lost his passport in Ottawa over All-Star Weekend, placing him in limbo for a few hours before matters could be sorted out. The story took life on twitter with the hashtag: freejoehaggerty.
Ever ready to hit the big time, The Great American Hockey Show seized the moment, producing a dramatized trailer to entice Hollywood into making a feature-length film.
Haggerty gives a synopsis of the true story at the beginning of this video, leading into the trailer. A more detailed account can be found in print.


text:
Wenger praises young side
Arsene Wenger has declared himself to be more than satisfied with his Arsenal side after a draw in Prague.
Last Updated: 08/11/07 7:28am
Arsene Wenger has declared himself to be more than satisfied with his Arsenal side after they secured their place in the last 16 of the UEFA Champions League.
A 0-0 draw against Slavia Prague was enough to book their passage into the competition's latter stages, with an inexperienced Gunners side doing the required job in the Czech capital.
Wenger was able to rest a high number of his key men and although Prague had a couple of decent chances, Arsenal looked comfortable for the most part.
The French tactician, who was taking charge of his 100th Champions League game, conceded Prague had worked hard for an impressive point of their own.
"They were solid at the back and they defended well. We had problems to create space and to be dangerous," he told Sky Sports News.
"We tried until the end to score but did not create enough to feel tonight that we can score goals.
Job done
"To win away from home in the Champions League is always difficult especially when a facing a team like that who felt humiliated - you face a tough game and on that side, you face a tough challenge.
"They did fight very hard and tried to stop us at any cost. Overall though, credit to them.
"I feel some players needed a breather, we come home qualified after four games and without conceding a goal."
Wenger reserved special praise for his goalkeeper Manuel Almunia, who responded to an uncertain display against Chelsea with an excellent stop in the second half.
"He made a key save and he knows how quickly in his position you have to take criticism and respond - with your performance on the pitch."


text:
Free music put to good use on The Daily English Show
Published on July 4 2008
Sarah is a New Zealander living in Japan. In addition to her teaching job, she started producing an online English lesson entitled The Daily English Show in April 2006. "The Daily English Show is an internet show for English students, English teachers and those interested in the English language and language study", she explains. Running a non profit operation, she obviously didn't have much of a budget for music, which is why she was thrilled to find in Jamendo an ideal source for background music, intros, etc. "It's usually very easy to find good stuff. We really love using music from Jamendo."
True to the spirit of Creative Commons licenses, every use of music on The Daily English Show is duly credited, and all the necessary links are posted. "We've had a lot of feedback from viewers thanking us for introducing them to the music and to Jamendo. We've also had great feedback from artists thanking us for using their music on the show. Our aim is to eventually generate income to make the show sustainable. When we do that, I hope to be able to make donations to the artists whose music we use."


text:
"Duppy Chunes unveils its female act 'She' in a brand new single titled 'Fine Boy'
Gift Halimbelo known by her stage name 'She'. The half Nigerian – half Ghanaian is a singer, songwriter, recording/performing artist, and an actress. She has a versatile genre of music ranging from Dance-hall, Reggae, and Contemporary Afro.
'She' is affiliated with Duppy Chunes records and unleashes her debut single produced by Orbeat accompanied with a video which was directed by Unlimited LA.


text:
1. processing of expatriate and local requisition.
2. using the requisition log for easy tracking and references of expatriate and local movement and travel schedules.
3. processing of craft requisition form (CRF) and using the CRF log for easy n tracking references.
4. relating with the human resource department in houston, london, warri and lagos and different personnel management issues.
5. sending hard copies and also scanning of personnel related documents to HR/personnel officer in companies main office 4 final processing.
6. keeping track of all mobilazation and demobilization of employees.
7. processing of travel authorization(TA) received expatriate staffs, get them approved and sent to the travel officers /coordinators in companies main office for ticket issuing.
8. sending of expatriate international passport and other immigration document to our immigration officer in companies main office for further processing.
9. taking care of expatriate expense report.
10. processing of expatriate/nationals time sheet for onward transmitter to pay roll in companies main officer for the payment of personnel's wages.
11. processing of requisitions for materials and sending it to project control officer for further processing.
12. taking care of all pension issues that concern the personnel's on site and transmitting to pay roll officer in companies main office.
13. sending mails to logistics department for the booking of any personnel that is leaving or coming to site, other than his normal rotation.
14. sending leave application letters including employees department rotation adjustment update of personnel's leave application and also updating of personnel statues from time to time as may be requested.
15. notifying payroll on any personnel absentecism other than leave or rotation without delay.


text:
I won't post the details as there are several tables, but the general gist is:
In 1.19 dying an item would change the stats and add class restrictions. However a lot of players weren't happy with being forced to wear one colour for optimum results.
In 1.20 the dying process will become 3 step;
1) Create the item you want
2) Treat (re-synth) the item to gain the attriibutes you want (e.g. +Piety or + Mind)
3) Dye the treated item to the colour you want to wear
Note that you can only dye an item once. Though there are plans in 2.0 to be able to dye a single item multiple times
I am not sure if dyeing is a final process, i.e. once you dye an item it can't be treated to get bonus stats.
Edited, Nov 15th 2011 3:21am by Magnesium02


text:
ASPEN, Colo. — The state of the international political landscape is more unpredictable and uncertain now than it has been in 38 years.
That's according to Gen. Raymond T. Odierno, the Army's chief of staff, who spoke at the opening session of the Aspen Security Forum last week.
Odierno answered questions from The New York Times reporter David E. Sanger about national security, international politics and the future of the Army.
The state of world politics has come to a head in recent weeks with crises breaking out in the Ukraine, Israel, Syria, Iraq and Afghanistan.
"Since 2012, the world has not become a safer place," Odierno said.
Odierno attributed the recent surge in violence to the fact that many of the countries facing upheaval are tied together politically.
Most of the problems in Iraq that occurred since the U.S. pulled out troops stemmed from a lack of leadership. The leaders were replaced and that led Iraqi soldiers to question their purpose, causing some to defect. That essentially opened the door for the extremist group, known as the Islamic State in Iraq and Syria, he said.
"The lesson I learned was that military power cannot solve problems alone," Odierno said.
As for the crisis in Syria, that would have happened no matter what the U.S. had done, he said.
Odierno said the U.S. should pay close attention to the crisis in Ukraine and support the National Atlantic Treaty Organization.
"Militarily, it's a bit of a wake-up call for NATO," Odierno said.
Still, he said the U.S. should be careful before getting involved, because the issue is complex.
Meanwhile, the federal government's budget sequestration of 2013 has threatened to cut the size of the current Army. If personnel is cut further, Odierno will have to reevaluate the nation's current strategy, he said.
Ultimately, Odierno doesn't want to see a draft occur, but that could be triggered by a budget shortfall, he said. The Army today is more capable than the Army in the past because soldiers are better trained and serve longer than previous generations, which makes them more experienced, Odierno said.
"I think it's worth the investment," Odierno said of the voluntary Army.


text:
What is it about lacrosse that you think is especially
good for girls?
It's extremely empowering, you have to be in good physical and
mental shape. … There's a great ability for girls to learn from
their mistakes, to understand what you are supposed to do, help
your team. It's about being there for your teammates.
What would you do if your girls said they hated
I don't plan on being "dance mom" for lacrosse. Already they
come with me to events and practices. If they hated it, I would be
OK with it as long as they are doing something that keeps them
physically active and mentally active. I have found in my years of
coaching and mentoring youth that old phrase 'idle hands are the
devil's handiwork' comes into play. They need to be doing
something, not because I'm a crazy parent, it's because I want them
to lead healthy and happy lives. That's a big part of what we talk
about at both Lakeshore and IGLA.
How has lacrosse helped you be a better
The less time you have, you become so much better at time
management and using every moment that you have.
Best moment as a parent?
I feel like every time you are in the moment, you feel like this
is the best moment ever.
Your favorite out-and-about thing to do with your
I really love it when we go on family walks together. Anything
we can do all together. Whenever you can sit back and actually
watch your kids having a great time, it's awesome.
Let us plan your weekend with the best family events and activities in Chicagoland.
Start the week right with deals, prizes, parent life hacks and more delivered straight to your inbox.
Need last-minute ideas for a weekend of family fun? No worries. We've got you.
Get the inside scoop on the people, places and things we are loving right now.
Resources, tips, inspiration and more for parents of children with special needs.
Score exclusive offers from our fabulous advertisers.


text:
In order to receive information about your Personal Data, the purposes and the parties the Data is shared with, contact the Owner.
If you need more information and are willing to understand your rights, you can also view the complete version of this privacy policy, by clicking the link at the bottom of this page.
120 N WASHINGTON SQ STE 805 LANSING, MI 48933, email@example.com


text:
Confirmed Canadian E. coli Cases UpAug 7, 2008 | Parker Waichman LLP
E. Coli Infection Among People Who Ate At University Of Guelph
Yesterday we reported on yet another E. coli outbreak emerging in Canada. Now, the number of confirmed cases of E. coli infection among people who ate at the University of Guelph late last month has reached seven, with six hospitalizations. The health unit there is pending test results for a number of people—at least over one dozen—with possible infections. Al those confirmed infected with E. coli ate at the University of Guelph campus, but not all at the same location. The E. coli contamination seems to have occurred somewhere on or near July 23 in a kitchen that prepares and distributes food to a variety of university eateries.
"We have no evidence, to date, that there was continued contamination," said Dr. Nicola Mercer, acting medical officer of health for Wellington-Dufferin-Guelph Public Health. "We continue to look at all possible causes of this outbreak. But we believe that whatever was there is gone." Mercer said the health unit has not yet ruled out a food brought into the kitchen around the time of the contamination.
Escherichia Coli Is Lethal Can Cause Blood Poisoning
Strain O157:H7 of Escherichia coli is lethal and can cause blood poisoning, cystitis, septicemia, and death. In the US, E. coli is the leading cause of food-borne illness with about 73,000 people becoming infected and 61 people dying from E. coli each year. Last year alone, over 22 million pounds of beef and vegetables were recalled due to E. coli outbreaks. In Canada, strain O157:H7 killed seven people and sickened 2,300 in Walkerton, Ontario in a tainted-water scandal.
Escherichia coli is a relatively common bacteria found in the human digestive tract and is normally harmless; however, some strains, including those linked to food poisoning, such as O157:H7, are much more serious and, often, deadly. Worse, this strain is extremely contagious and only a small amount of bacteria can contaminate a large number of people. E. coli taints meat through improper butchering and processing practices and, once released in the body, produces a type of toxin that leads to severe bleeding and diarrhea, has been associated with kidney damage in young children, and can also lead to kidney failure and death. Symptoms of E. coli infection include stomach cramps and watery diarrhea that may turn bloody within one to three days. More and more, E. coli is turning up in produce and water.
Need Legal Help Regarding E. Coli Outbreak?
The personal injury attorneys at Parker Waichman LLP offer free, no-obligation case evaluations. For more information, fill out our online contact form or call 1-800-YOURLAWYER (1-800-968-7529).


text:
Each month, Rated People connects over 50,000 homeowners with quality tradesmen - simply enter your job details in the form above to get started.
We'll match your job to the relevant tradesmen in your area - those interested will pay to see your contact details and call you to quote.
As each tradesman expresses interest in quoting on your job, we'll send you their profile and ratings to help you choose the right one for you.
After the work is complete, return to the site and rate your tradesman based on their quality of work, reliability and value for money.
Tree Surgeon
Added 27/09/2015
High conifer hedge needs 3 feet off top - not a big area
Tree Surgeon
Added 18/04/2015
Pruning of 3 - 4 trees (branches primarily). Please contact me if further details required...
Tree Surgeon
Added 24/02/2014
Two 35/40 ft conifers/pines? to be removed from front garden - good clear access. Had a single...
Tree Surgeon
Added 26/01/2014
I need a fallen Sycamore tree removed and the stump ground out. The fallen tree is in the...
Managing your job is easier with the Rated People Homes App, download it today.