The Canadian Social Enterprise Guide is available for free on http://www.enterprisingnonprofits.ca/guide_form . As said on EPN website, the original Social Enterprise Guide was originally published in 2006 and was the first extensive and comprehensive published resource, tool kit, and collection of social enterprise stories in Canada. The revised 2nd Edition of the Guide reflects the learning of Enterprising Non-Profits program and its 10 years of supporting the development and success of social enterprise through technical assistance and resource development. The Guide includes chapters written by enp staff, social enterprise practitioners, professional trainers, funders and organizational development professionals.
If you're a non-profit organization thinking about creating or already developing a new enterprise, or if you are expanding/formalizing your existing revenue-generating programs, then this Guide is for you. As a social enterprise development and planning tool the Guide is valuable for project managers, executive directors, Board members, and staff of a wide range of non-profit organizations. The Guide is also useful for business classes, students, corporate social responsibility businesses, government, industry, consultants/trainers and funders.
Why we wrote this Guide….
– How can you tell if your group is ready to embark on a social enterprise?
– What are the steps in a social enterprise planning process?
– How do you identify and assess enterprise opportunities?
– How do you plan for a social enterprise?
– How can you measure social returns in a business setting?
– What do you need to know about the legal context?


text:
\section{Inferring Concise Postconditions}
\label{sec:technical-approach}
\label{sec:our-approach}

Figure \ref{fig:overview-pipeline} shows an overview of our approach for
inferring postconditions that consists of the following steps.
\begin{enumerate}
	\item The input is the code of the API method for which postconditions are needed.
	      If preconditions are available, they can also be provided.
	      Otherwise, our approach starts with the default precondition \textbf{\texttt{true}}.
	\item Next, the code is symbolically
	      executed to produce traces. The symbolic execution uses the strongest postcondition predicate transformer semantics (SP).
	      These traces are converted to a raw specification. (See Sec.~\ref{subsec:sp} below.)
	\item Then, we flatten the raw specification into groups of clauses (cases).
		  (See Sec.~\ref{subsec:flattening})

	\item Next, we compute the overlapping states found between groups of clauses. (See Sec.~\ref{subsec:state-finding}.)

	\item Finally, we recombine states and convert the results to
          the final specification. (See Sec.~\ref{subsec:recombining}.)

\end{enumerate}

\subsection{Producing Raw Specifications}
\label{subsec:sp}

We use forwards symbolic execution \cite{gordon_forward_2010} to symbolically
execute the annotated AST of each API method.
The rules used by our symbolic execution engine are shown in Fig.~\ref{fig:rules}.

\input{figures/rules}

A challenge in this step was to avoid existential quantifiers in SP's output.
Existential quantifiers are problematic because they require the use of a constraint solver.
However, the assignment rule in Equation \ref{eqn:ass} in Fig.~\ref{fig:rules} uses an existential quantifier.  We avoid this problem by using a type of program representation called the ``Optimal Passive Form'' \cite{grigore_strongest_2009,leino_this_2008,barnett_weakest-precondition_2005}.
In Optimal Passive Form, which is a variant of single static assignment (SSA) form,
in which every assignment to a variable results in a new variable.
In addition to simplifying the control flow graph of a program, this form eliminates the need for such existential quantifiers since one does not need to search for previous assignments of variables when making new assignments.
Next, we convert the propositions produced by SP into a raw specification.
We define an abstract form of specifications independent of any concrete specification language,
such as JML.
The specifications themselves are to be thought of as method specifications.
The only interesting properties we assume about specifications are that one can extract cases (such as those produced by $SP$) from a specification
and that each such case has a set of preconditions (conceptually a conjunction) and a set of other clauses (also conjoined).
Thus each specification is modeled as a non-empty list of cases, separated by a special operator $\vee$.
Within a case, clauses such as preconditions and postconditions are modeled as ``atomic formula,''
assertions whose structure is not further examined.
This step produces specifications in a form that we call {\em specification normal form} (SNF).
While specifications allows preconditions to distribute over cases,
in SNF no such distribution of preconditions is allowed;
thus in SNF each case is a non-empty list of cases, each separated by the operator $\vee$.

\begin{definition}[Specification Normal Form (SNF)]
	\label{def:snf}
	A specification is in \emph{specification normal form (SNF)} if it follows the grammar in Figure~\ref{fig:snf-grammar}.
	\input{figures/snf-grammar}
\end{definition}

To illustrate this phase of our technique consider the function in Figure~\ref{fig:cmp}.
The computation of $\metaop{sp}(\texttt{cmp},\phi)$ produces the following formula:

\begin{equation}\label{eqn:sp-computed}
\begin{array}{l}
(a < b \land \phi \land \KW{result} = -1) \\
~ \lor \: ( (a > b \land \lnot(a < b) \land \phi \land \KW{result} = 1) \\
~ \lor \: (\lnot(a < b) \land \lnot (a > b) \land \phi \land \KW{result} = 0))
\end{array}
\end{equation}

Formula~(\ref{eqn:sp-computed}) corresponds to the following specification.

\begin{equation}\label{eqn:sp-computed-spec}
\begin{array}{l}
(\PREREST{a < b \land \phi}{\KW{result} = -1}) ~\vee \\
\: (\PREREST{a > b \land \lnot(a < b) \land \phi}{\KW{result} = 1}) ~\vee \\
\: (\PREREST{\lnot(a < b) \land \lnot (a > b) \land \phi}{\KW{result} = 0})
\end{array}
\end{equation}

\subsection{Flattening Specification Cases and Computing Weights}
\label{subsec:flattening}

\input{far-algorithm}

Algorithm \ref{alg:far} describes the next three components of our technique.
The input of this component is the raw specification produced by the predicate transformer semantics in SNF.

In the first step of the algorithm,
these clauses are placed in a data structure suitable for a graph-based analysis;
our implementation uses the JPaul program analysis library \cite{jpaul}.

First we collect the cases of the specification, represented as $\metaop{cases}$ in
Algorithm \ref{alg:far}, as a set.
The semantics of case extraction is as follows.
\begin{displaymath}
\begin{array}{l}
\metaop{cases} : \domain{Specification} \rightarrow \POWERSET{\domain{Case}} \\
\metaop{cases}(S) \stackrel{{\rm def}}{=} \LETHEAD{c_1 \vee \ldots \vee c_n}{S} \{ c_1, \ldots, c_n \}
\end{array}
\end{displaymath}

With the cases of the specification collected, the next step is to flatten the specification. This is done by taking each case of the raw specification and detaching it from the tree. This forms a disjoint forest of all the specifications cases.

Once flattening is complete, Strongarm computes weights for each specification case
using an equivalence relation on pairs of distinct cases as shown in Algorithm \ref{alg:to-graph}.
On Line 7 of Algorithm \ref{alg:to-graph} this equivalence relation is denoted by the symbol `$\sim$'. For simplicity, our prototype uses lexical identity for the relation $\sim$.
In our experimental analysis (Section \ref{sec:technical-evaluation}) we find that this choice works out well.\footnote{The $\sim$ relation used need not be lexical identity; we speculate that more interesting results could be achieved by considering other relations, such as logical equivalence, but that is beyond the scope of this paper.}
The weights assigned are the number of preconditions that are $\sim$ between the two cases;
for example, if cases $l$ and $r$ have 3 preconditions that are related by $\sim$, then the weight assigned to the edge from $l$ to $r$ is 3.
In Fig.~\ref{fig:overview-pipeline}, an edge of weight $n$ is shown as $n$ dashed edges.

\subsection{State Finding}
\label{subsec:state-finding}

Returning to Algorithm \ref{alg:far},
the next step is to compute the connected components of the resulting graph. In Figure \ref{fig:overview-pipeline}, this process produces Component 1 and Component 2.

\subsection{Recombining and Conversion to Contract}
\label{subsec:recombining}

The next step of Algorithm \ref{alg:far} selects, from each connected component, the pair of vertices with the largest weight edges connecting them (i.e., the most similarity), by calling \texttt{MergeSCC} (Algorithm \ref{alg:mergescc}).
For example, in Figure \ref{fig:overview-pipeline} this produces the choice $(C_6,C_7)$ for Component 1 and $(C_2,C3)$ for Component 2.

Algorithm \ref{alg:mergescc} works on each connected component as follows.
First it selects from the connected component, the maximum weight (Line~3),
and a pair of vertices connected by an edge with that weight (Line~4).
The selected pair of verticies are combined into a single node by extracting the common preconditions between the two verticies
(Line~6) and returning a modified residual graph with an edge connecting the common preconditions
($c$) to both verticies without those common specifications ($L'$ and $R'$, Lines~9 to 13).
For example, in Fig.~\ref{fig:overview-pipeline} $C_2$ and $C_3$ are combined into a single node, as are $C_6$ and $C_7$.
Next, we examine the connected component to which the pair belongs. If any vertex is adjacent to any of the elements of the pair, we remove that edge from the graph (Line~15).

Upon returning to Algorithm \ref{alg:far}, Lines~11 to 12 make a root node for the specification.
When converted to a specification, this root node will be a disjunction ($\vee$) of all the newly-created conjunction nodes
(the merged states in Fig.~\ref{fig:overview-pipeline}). In the example in Figure \ref{fig:overview-pipeline}, this leaves us with vertices $C_1$ and  $C_5$.
This subgraph is then fed back into the FAR algorithm until there are no remaining vertices. Completely disjoint vertices (those with no preconditions in common with any of the other vertices) form a disjoint forest in the final iteration of the algorithm. Once this outcome is reached, each vertex in the forest is connected unmodified to the root. This resulting tree is then converted back into a specification.

\subsection{Soundness of Our Approach}
\label{subsec:soundness-brief}

We have proved the soundness of our approach in a detailed report.
Briefly, soundness for our approach is defined with respect to satisfaction by programs (method bodies).
In essence a program $C$ satisfies a specification $S$ if for every pre-state $s$ that satisfies some case $c$'s precondition, the semantics of $C$ is such that the post-state $s'$ that $C$ produces (when run on $s$) satisfies $c$'s postcondition.
The $FAR\xspace$ algorithm uses an equivalence relation $\sim$ to compute
the intersection between two sets of preconditions.
However, not just any equivalence relation on atomic formulas will do; a \emph{sound} relation must preserve the meaning of atomic formulas.
Lexical equivalence is sound. Our report shows that if $\sim$ is sound, then
the semantics of specifications is preserved by Algorithm \ref{alg:far}.

\subsection{Implementation Details}
\label{subsec:implementation-details}
After an execution trace of an API method is obtained, we need to transform the trace and the underlying predicate AST into a raw specification.
Our implementation includes several transformation tasks such as translation from internal variable representations to externalized (source code level) representations, removal of tautologies, determination of purity, and inference of frame axioms. For space considerations we omit a detailed description of these techniques.

\section{Related Work}
\label{sec:related-work}

In addition to the work discussed in Section \ref{sec:introduction}, there are several other systems and papers relevant to this paper. The closest related work to Strongarm is the Houdini system by Flanagan and Leino \cite{flanagan_houdini_2001}. Houdini targets ESC/Java with the goal of statically inferring specifications for Java. Similarly, in our work we target OpenJML, a successor to ESC/Java. However, rather than symbolically computing specifications as Strongarm does, Houdini instead applies templates, i.e., commonly-found specification patterns; to search for a specification, Houdini tries all of these patterns and checks the candidate specifications using ESC/Java. In contrast to Strongarm, Houdini also attempts to infer object invariants using the same mechanism, which Strongarm does not yet attempt.

Flanagan and Saxe's work on compacting verification conditions \cite{flanagan_avoiding_2001}, unlike Strongarm, only deals with two types of duplication: multiple assignment and propagation of accumulated formulas.  Strongarm can reduce these problems globally in the specification whereas the approach of Flanagan and Saxe is restricted to the branch level. Furthermore, Strongarm uses a pluggable equivalence relation ($\sim$, see Section \ref{subsec:flattening}), which generalizes their work.

In contrast with Strongarm (and Houdini), Daikon \cite{ernst_daikon_2007} is a runtime approach. To produce specifications, Daikon requires a test suite that calls the code that is being targeted for inference. Even when such a test suite is available, dynamic inference can fail, since code coverage and branch coverage are typically not sufficient to produce specifications \cite{harder_improving_2003,gupta_new_2003}, as many test suites focus on corner cases and are thus not suitable for specification inference \cite{nimmer_invariant_2002}.

Similarly, in their work on discovering relational specifications, Smith et al. discover specifications by looking at program outputs \cite{smith_discovering_2017}. Our approach is fully static does not require running the code.

In their work on API usage error detection, Murali et al. investigate detecting API usage errors  using Bayesian inference \cite{murali_bayesian_2017}. Our approach does not use machine learning to generate its specifications and therefore does not require training examples to infer specifications.

Nguyen et al.~\cite{nguyen_mining_2014-1} infer method preconditions, by examining call sites. Our approach is different in that Strongarm computes postconditions based on each method's code, not preconditions based on calling code.

\section{Conclusion and Future Work}
\label{sec:conclusion}

Our approach to inferring practical postconditions takes advantage of structure the logical formulas that result from the SP predicate transformer. We evaluated our technique on 7 popular Java libraries and found that 95.0\% of the inferred specifications were less than 1 page long and 84.6\% were less 1/4 of a page.
Such concise specifications have the potential aid many areas of software engineering.
Our future work will evaluate these implications.

\section{The FAR\xspace Algorithm}
\label{sec:soundness}\label{sec:far-algorithm}

The main problem with formulas computed by \textit{sp} is that when the results are converted into specifications, they can become very large, deeply nested, and repetitive. At each branch point in the program the branch's precondition is fed back into \textit{sp} (see Equation \ref{eqn:if}) as an argument, which causes the number of specification cases in the resulting specification to grow exponentially. In this section we describe the Flattening and Recombination (FAR) algorithm that produces an equivalent specification that is shorter and more practical than the input specification.

In this section we discuss the FAR\xspace algorithm and soundness of the results produced by FAR\xspace and develop a theorem about its soundness. We say that FAR\xspace is \emph{sound}
if the specification that results from running FAR\xspace is equivalent to its argument specification. By \emph{equivalent} we mean that the set of programs satisfying the argument specification is the same as the set of programs satisfying the resulting specification.

The outline of this section is as follows. First, in Section \ref{sec:specs-as-boolean-formulas}, we discuss the connection between JML specifications and first order Boolean formulas and describe our meaning of the specifications that FAR\xspace operates on. As we shall discuss, the soundness of FAR\xspace depends on the soundness of $\sim$, and in Section \ref{sec:soundness-of-tilde} we will discuss the soundness property of $\sim$ used in FAR\xspace. Lastly, in Section \ref{sec:soundness-of-far} we discuss the soundness theorem of FAR\xspace.

\subsection{Abstract Specifications}
\label{sec:specs-as-boolean-formulas}\label{sec:abstract-specifications}

In discussing the soundness of FAR\xspace, it is useful to abstract the specifications FAR\xspace operates on from particular specification languages. In this section we discuss the formal details of the kinds of specifications FAR\xspace operates on and produces independent of a particular specification language.
The specifications themselves are to be thought of as method specifications.
The only interesting properties we assume about specfications are that one can extract cases (such as those produced by $SP$) from a specification
and that each such case has a set of preconditions (conceptually a conjunction) and a set of other clauses (also conjoined).
Thus each specification is modeled as a non-empty list of cases, separated by a special operator $\vee$.
Within a case, each clause is modeled as an ``atomic formula,''
which can be thought of as an assertion whose structure is not further examined; $FAR\xspace$ treats atomic formulas as variables.
Specifications allow preconditions to distribute over cases, but in specification normal form (SNF), which is the format of the output of $\metaop{sp}$ and the input of $FAR\xspace$, no such distribution of preconditions is allowed;
thus in SNF each case is a non-empty list of preconditions and other clauses, each separated by the operator $\wedge$. However, in specifications in general $\wedge$ can be used to distribute preconditions over other specifications.

The semantics of specifications is most easily understood for the simple case of SNF, where the intuition is that for a specification of the form
$a \vee b \vee c$,
if the preconditions of each of the cases $a$, $b$, and $c$ are never true in the same pre-state, then an implementation that transforms a pre-state $s$ into a post-state $s'$ is correct if the pair of states $(s,s')$ satisfies the non-preconditions of the case whose precondition was true in the pre-state $s$. This semantics the same as JML's \lstinline!also! operator when the preconditions are disjoint, and the outputs of $SP$ and $FAR\xspace$ always have disjoint preconditions.
A specification of the form $\CREATEDISTRIB{p}{S}$, is an abbreviation for distributing the precondition $p$ into each case of $S$, and thus simply adds the precondition $p$ to each specification case of $S$.

\begin{definition}[A Specification Language]
  \label{def:spec-language}
A \emph{specification language} is a language modeled by a set of expressions, $\domain{Exp}$, a set of type expressions, $\domain{TypeExp}$, that includes $\domain{Boolean}$, a set of type environments, $\domain{TypeEnv}$, a typing judgment, $\vdash$, a set of states, $\domain{State}$, and, for each type environment $\Gamma \in \domain{TypeEnv}$ a meaning function for expressions, ${\cal E}_{\Gamma}$.
Type environments $\Gamma\in\domain{TypeEnv}$ are maps from names to $\domain{TypeExp}$.
Typing judgments of the form $\Gamma \vdash E : \tau$ relate a type environment ($\Gamma$), an expression ($E$), and a type expression ($\tau$).

Boolean-valued expressions are called \emph{atomic formula}:
\begin{displaymath}
\domain{AtomicFormula} \stackrel{{\rm def}}{=} \{ E \mid E \in \domain{Exp}, \exists \Gamma \in \domain{TypeEnv} . \Gamma \vdash E : \domain{Boolean} \}.
\end{displaymath}
Since some atomic formulas may relate a pre-state to a post-state,
the meaning function for expressions that type check in a type environment $\Gamma$, ${\cal E}_{\Gamma}$, takes two states as an argument.
For a given type environment $\Gamma$,
\emph{$\Gamma$-state}s $s$ and $s'$ are states that agree with the type environment $\Gamma$ in the sense that for each expression $E$,
if $\Gamma \vdash E : \tau$, then $\ME{\Gamma}{E}(s,s')$ is an element of the meaning of the type $\tau$.

\end{definition}

We use the notation $\metaop{cases}$ to extract the cases of a specification as a set.
\begin{displaymath}
\begin{array}{l}
\metaop{cases} : \domain{Specification} \rightarrow \POWERSET{\domain{Case}} \\
\metaop{cases}(S) \stackrel{{\rm def}}{=} \LETHEAD{c_1 \vee \ldots \vee c_n}{S} \{ c_1, \ldots, c_n \}
\end{array}
\end{displaymath}

Sometimes it will be convenient to use operators $\metaop{pre}$ and $\metaop{rest}$ to extract the precondition and other atomic formulas (e.g., the postcondition) from a case; they have types:
\begin{displaymath}
\begin{array}{l}
   \metaop{pre} : \domain{Case} \rightarrow \POWERSET{\domain{AtomicFormula}} \\
   \metaop{rest} : \domain{Case} \rightarrow \POWERSET{\domain{AtomicFormula}}.
\end{array}
\end{displaymath}
These operations satisy, for all $P,Q \in \POWERSET{\domain{AtomicFormula}}$, and $S\in\domain{Specification}$,
\begin{align}
    \metaop{pre}(\CREATE{P}{Q}) & = P \\
    \metaop{rest}(\CREATE{P}{Q}) & = Q \\
    \metaop{pre}(\CREATEDISTRIB{P}{S}) & = P \cup \left( \bigcup_{c\in\metaop{cases}{S}} \metaop{pre}(c)\right) \\
    \metaop{rest}(\CREATEDISTRIB{P}{S}) & = \bigcup_{c\in\metaop{cases}{S}} \metaop{rest}(c).
\end{align}

A restriction of the greneral form of specifications defines the output format of $\metaop{sp}$ and thus the input format of $FAR\xspace$. This format does not allow preconditions to be combined with specifications using $\wedge$.

\subsection{Connection with SP}

The foundation of the connection between a specification languages
and the abstract specifications described in Section~\ref{sec:abstract-specifications}
and the formulas produced by $\metaop{sp}$ is straightforward, because $\metaop{sp}$ produces formulas in disjunctive normal form in which the formulas corresponding to preconditions are all disjoint.

Consider the contract in Listing \ref{fig:cmp-normal-spec}. In this contract, although the symbols are different, we can see terms that correspond to the terms found in the result of $\metaop{sp}$ in formula (\ref{eqn:sp-computed}) and the corresponding abstract specification in formula (\ref{eqn:sp-computed-spec}). Specifically, note that the three parts of the JML specification that are separated by ``\KW{also}'' in Listing \ref{fig:cmp-normal-spec} correspond to the three cases (separated by $\vee$) of the abstract specification in formula (\ref{eqn:sp-computed-spec}). The translation to JML is very direct in this way.

For specification languages that do not have JML's specification cases it is still possible to use the output of FAR to make the specificaions shorter. This would be done by translating a formula like formula (\ref{eqn:sp-computed-spec}) into a single postcondition, using a translation function $\metaop{Tr}$ defined on specificaitons and cases as follows:

\begin{displaymath}
\begin{array}{l}
  \metaop{Tr}(c_1 \vee \ldots \vee c_n) = \metaop{Tr}(c_1) \land \ldots \land \metaop{Tr}(c_n) \\
  \metaop{Tr}(\PREREST{p}{q}) = (\KW{old}(p) \Rightarrow q) \\
  \metaop{Tr}(\PREDISTRIB{p}{S}) = (\KW{old}(p) \Rightarrow \metaop{Tr}(S))
\end{array}
\end{displaymath}

Note the use of $\land$ instead of $\vee$ in the produced postcondition to connect cases. If this were not done, then the postcondition would be trivially satisfied whenever one of the preconditions was false.
(Also for the distributed form of specification cases $\PREDISTRIB{p}{S}$,
note that $p \Rightarrow (p' \Rightarrow q)$ is equivalent to $p \land p' \Rightarrow q$, so the first precondition ($p$) distributes over the others as required.)
For example, formula (\ref{eqn:sp-computed-spec}) would turn into the following postcondition

\begin{equation}\label{eqn:sp-non-JML}
\begin{array}{l}
  (\KW{old}(a < b \land \phi) \Rightarrow (\KW{result} = -1)) \\
 ~ \land \: (\KW{old}(a > b \land \lnot(a < b) \land \phi) \Rightarrow (\KW{result} = 1)) \\
 ~ \land \: (\KW{old}(\lnot(a < b) \land \lnot (a > b) \land \phi) \Rightarrow (\KW{result} = 0))
\end{array}
\end{equation}

\subsection{Soundness of $\sim$}
\label{sec:soundness-of-tilde}

The $FAR\xspace$ algorithm uses an equivalence relation $\sim$ to compute
the intersection between two sets of preconditions.
However, not just any equivalence relation on atomic formulas will do; the relation must preserve the meaning of atomic formulas.

\begin{definition}[Sound Equivalence Relation]
\label{def:tilde-r}
An equivalence relation $\sim$ on atomic formulas is \emph{sound} iff for all type environments $\Gamma$ and all atomic formulas $F$ and $G$ such that
$\Gamma \vdash F : \domain{Boolean}$ and $\Gamma \vdash G : \domain{Boolean}$:
\begin{displaymath}
  F \sim G \Rightarrow \forall \Gamma\textrm{-states } s, s' \: . \:
     \ME{\Gamma}{F}(s,s') = \ME{\Gamma}{G}(s,s').
\end{displaymath}
\end{definition}

The $FAR\xspace$ algorithm works correctly if $\sim$ is any sound equivalence relation on atomic formulas. However, in this paper and our implemention we use lexical equivalence (i.e., textual identity) as the relation,
hence we need the following corollary, whose proof is trivial.

\begin{corollary}[Soundness of Lexical Equivalence]
  \label{lem:soundness-of-le}
  Lexical equivalence of atomic formulas is a sound equivalence relation.
\end{corollary}

\subsection{Soundness of FAR\xspace}
\label{sec:soundness-of-far}

In this section we show the soundness of FAR\xspace. Since soundness for $FAR\xspace$ is defined with respect to satisfaction by programs (method bodies), we first define satisfaction for programs. In essence the following definition says that a program $C$ satisfies a specification $S$ if for every pre-state $s$ that satisfies some case $c$'s precondition, the semantics of $C$ is such that the post-state $s'$ that $C$ produces (when run on $s$) satisfies $c$'s postcondition.

\begin{definition}[Satisfies a Specification] \label{def:models}
Let $\Gamma$ be a type environment. Let $S$ be a specification in which each atomic formula contained in $S$ type checks in $\Gamma$.
Let $C$ be a program whose semantics is captured by a state transformer $\chi$ that transforms $\Gamma$-states to $\Gamma$-states.
Then \emph{$C$ satisfies $S$}, written $C \MODELSWRT{\Gamma} S$,
if and only if for all $\Gamma$-states $s$ such that there is a case
$c \in \metaop{cases}(S)$ such that for each atomic formula $p \in \metaop{pre}(c)$,
$\ME{\Gamma}{p}(s,s)$ is true,
and $\chi(s) = s'$, then for each atomic formula $q \in \metaop{rest}(c)$,
$\ME{\Gamma}{q}(s,s')$ is true.
\end{definition}

The following lemma relates to the invariant of the $FAR\xspace$ algorithm that we use to prove its soudness.

\begin{lemma}[\ToSpecification on Flat Tree] \label{lem:flat-tree}
  Let $G$ be a graph $\langle V,E \rangle$ with root $G.root$ such that $\forall v \in V~ \langle G.root, v \rangle \in E$. Then $\ToSpecification(G, G.root)$ produces the disjunction of each $v \in V$.
  \end{lemma}
  \begin{proof}
    Let $G$ be a graph $\langle V,E \rangle$ with root $G.root$ such that $\forall v \in V~ \langle G.root, v \rangle \in E$. On Line \ref{ln:foreach-adjacent}, \ToSpecification iterates over each vertex in $G$. On Line \ref{ln:isaleaf}, we test if $v$ is a leaf. Since all $v$ are leaves, on return on Line \ref{ln:return-tospecification}, $B$ contains the set $V$. Since $\bigvee B$ produces the disjunction of every element of $B$, $\ToSpecification(G, G.root)$ produces the disjunction of each $v \in V$.
  \end{proof}

The following corollary also relates to the invariant in the $FAR\xspace$ algorithm.

  \begin{corollary}[Two-Leaf Pairs Converted to Specifications]
    \label{col:logical-relation-of-any-two-v}
    Let $G$ be a graph $\langle V,E \rangle$ with root $G.root$. For any pair of leaf vertices $(l,r)$ adjacent to $G.root$, $\ToSpecification(G, G.root)$ contains a disjunction of $l$ and $r$ if and only if $\{l,r\} \subseteq V$.
  \end{corollary}

The following definition of soundness for $FAR\xspace$ is reasonable because if $FAR\xspace$ does not change the meaning of a specification, then it is only simplifying it. Furthermore, since we pass specifications to $FAR\xspace$ that are derived from $\metaop{sp}$ and these capture the behavior of the code, if $FAR\xspace$ does not change the meaning of these specifications, then they still capture the behavior of the code.

\begin{definition}[Soundness of FAR\xspace]
\label{def:soundness-of-far}
Let $\sim$ be a sound equivalence relation on atomic formulas.
Then \emph{$FAR\xspace$ is correct with respect to $\sim$} iff for all programs $C$ and for all specifications $S$:
    $$C \MODELSWRT{\Gamma} S \iff C \MODELSWRT{\Gamma} FAR\xspace(S,\sim).$$
\end{definition}

\begin{theorem}[FAR is Sound]
  \label{theo:far-is-sound}
  If $\sim$ is a sound equivalence relation, then FAR\xspace is correct with respect to $\sim$.
\end{theorem}
\begin{proof}
  Assume $\sim$ is a sound equivalence relation. Let $\Gamma$ be a type environment. Let $C$ be a command with semantics $\chi$ that takes $\Gamma\text{-states}$ to $\Gamma\text{-states}$. Let $S$ be a specification in SNF in which each atomic formula contained in $S$ typechecks in $\Gamma$.

The proof uses a loop invariant maintained by FAR\xspace. FAR\xspace maintains the state of its execution according to the tuple $\langle S, V, Residual \rangle$, where $V$ is a list of unmerged vertices and $Residual$ is the residual graph formed from previous $MergeSCC$ calls. We refer to the state $\langle S, V, Residual \rangle$ as $FAR\xspace_{State}$ and define the following invariant that operates on its elements:

  \begin{displaymath}
    \begin{array}{l}
    \metaop{inv} : \domain{Specification} \rightarrow \{Case\} \rightarrow Graph \rightarrow \domain{Boolean} \\
    \metaop{inv}(S, V, G) \stackrel{{\rm def}}{=} \: \LETHEAD{G'}{\langle G.V \cup V, G.E \cup \{(G.root, v) ~|~ v \in V\} \rangle} \\
    ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ \:  C \MODELSWRT{\Gamma} S \iff C \MODELSWRT{\Gamma} FAR\xspace(\ToSpecification(G', G'.root),\sim)

    \end{array}
    \end{displaymath}

    The graph $G'$ formed in \metaop{inv} by $\langle G.V \cup V, G.E \cup \{(G.root, v) ~|~ v \in V\} \rangle$ encapsulates Lines \ref{ln:far-makeg-1} and \ref{ln:far-makeg-2} of FAR\xspace which are responsible for taking the remaining elements of $V$ and adding them to the residual graph. As can be seen on Line \ref{ln:far-makeg-1} they are added to the root of $Residual$. Encapsulating the end of the FAR\xspace procedure in this way demonstrates what a snapshot of the state of FAR\xspace would be for any given iteration of the loop on Line \ref{ln:far-loop}.

  \textit{Establishing.} The invariant \metaop{inv} is established after the execution on the statement on Line \ref{ln:inv-established} of Algorithm \ref{alg:far}. At this point $FAR\xspace_{State} = \langle S, \metaop{cases}(S), \langle \emptyset, \emptyset \rangle\rangle$. In \metaop{inv}, since $G$ is empty, $G'$ is a graph with a root that is attached via an edge to each leaf in $V$. By Lemma \ref{lem:flat-tree}, we know that $\ToSpecification(G', G'.root)$ is the disjunction of all of the cases of $V$. While this may reorder the cases, the semantics of a speicification is unaffected by the order of the cases, therefore the invariant is established.

  \textit{Maintaining.} Lines \ref{ln:far-loop1} and \ref{ln:far-loop2} have no effect on the values of $FAR\xspace_{State}$ and therefore do not directly affect the value of \metaop{inv}. We are concerned with the effect of the computation on Line \ref{ln:far-loop3}. The result of Line \ref{ln:far-loop3} is impacted by the value of $V$, the value of which takes on several cases.
  \begin{description}
    \item[Case 1] Consider $V = \emptyset$. In this case $\MergeSCC(V, W, Scc, Residual, \sim) = \langle V, Residual \rangle$. That is, $\langle V, Residual \rangle$ is not modified. This case is trivial since the connected component of an empty graph is empty as well. In this case $\langle V, Residual \rangle$ is not modified and hence $FAR\xspace_{State}$ remains the same.
    \item[Case 2] Consider $V \neq \emptyset$ and for every pair $(l,r) \in V \times V$  such that $l \neq r $ the formula $|\{ (x,y) \in \metaop{pre}(l) \times \metaop{pre}(r) ~|~ x \sim y\}| = 0$ is true. In this case, for each iteration of the loop of Algorithm \ref{alg:to-graph}, the condition on Line \ref{ln:to-graph-branch} is false. This case is equivalent to case 1, since there are no edges and therefore the graph is a disjoint forest. In this case, the connected components all contain one vertex. However, since the loop on Line \ref{ln:merge-loop} of Algorithm \ref{alg:mergescc} only executes in the event $|Component.V| > 1$, the pair $\langle V, Residual \rangle$ is not modified and hence $FAR\xspace_{State}$ remains the same.

    \item[Case 3] Consider $V \neq \emptyset$ and there exists some pair $(l,r) \in V \times V \text{ such that } l \neq r $ where $|\{ (x,y) \in \metaop{pre}(l) \times \metaop{pre}(r) ~|~ x \sim y\}| > 0$. In this case, at least one component of $Scc$ will satisfy the requirement $|Component.V| > 1$ of the loop on line \ref{ln:merge-loop} of Algorithm \ref{alg:mergescc}. We consider the effect of a single component on the value of \metaop{inv}. Let the pair selected on Line \ref{ln:select-pair} be the pair $(L,R)$. Let $common$ be the set $\{ l ~|~ (l,r) \in \metaop{pre}(L) \times \metaop{pre}(R)$ where $l \sim r\}$ computed on Line \ref{ln:common} of Algorithm \ref{alg:mergescc}. On exit from Line \ref{ln:mergescc-remove-v} of Algorithm \ref{alg:mergescc} $FAR\xspace_{State} = \langle S, V', Residual' \rangle$ where the following updates have been made:

    \begin{itemize}
      \item[] $V' = V \setminus (\{R\} \cup \{L\}) \Rightarrow \ToSpecification(Residual, Residual.root) $ does not contain $L \lor R$ (by Corollary \ref{col:logical-relation-of-any-two-v}), which causes \metaop{inv} to no longer hold.
    \end{itemize}

However, the following computation causes \metaop{inv} to hold again:

\begin{itemize}
  \item[] $Residual'.E = Residual.E \cup (\{common\} \times \{L', R'\}) \cup \{(Residual.root, common)\}$
  \item[] $Residual'.V = Residual.V \cup \{L\} \cup \{R\}$
  \item[] $\mathbf{where} $
  \begin{itemize}
    \item[] $L' = \PREREST{(pre(L) \setminus common)}{rest(L)}$
    \item[] $R' = \PREREST{(\metaop{pre}(R) \setminus \{r ~|~ (l,r) \in \metaop{pre}(L) \times \metaop{pre}(R) \text{ where } l \sim r\})}{\metaop{rest}(R)}$
  \end{itemize}
\end{itemize}

    On Line \ref{ln:mergescc-remove-v}, $L$ and $R$ are removed from $V$. Prior to removal, an evaluation of \metaop{inv} would produce a disjunction of $L$ and $R$ from Corollary \ref{col:logical-relation-of-any-two-v} in the final specification. They are replaced in $Residual$ by something that translates to an equivalent specification. That is, the formula  $(L \lor R)$ is replaced by $(common \land (L' \lor R'))$ on Lines \ref{ln:replace-v1} and  \ref{ln:replace-v2} when $Residual$ is updated. Since $\sim$ is a sound equivilance relation, $(L \lor R) \equiv (common \land (L' \lor R')) \Rightarrow \metaop{inv}(S,V,Residual)$ and therefore the invariant \metaop{inv} is maintained.

  \end{description}

  \textit{Terminating.} In the case evaluation in the maintaining step, we showed how \metaop{inv} holds at each step of the loop in FAR\xspace. Since Lines \ref{ln:far-makeg-1} and \ref{ln:far-makeg-2} are encapsulated by \metaop{inv}, we know that \metaop{inv} holds on exit from FAR\xspace which gives us the desired result.
\end{proof}

\section{Discussion}
\label{sec:discussion}

\section{Future Work} \label{sec:future-work}

\section{Acknowledgments} \label{sec:acknowledgments}
The work of Anonymous Authors was supported in part \blackout{by NSF grants NNNNNNN and NNNNNN. The work of Anonymous Authors was also supported by NSF grants NNNNN and NNNNNN}.

This material is based upon work supported by the National Science Foundation under Grant No. \censor{NNNNNNN}. Any opinions, findings, and conclusions or recommendations expressed in this material are those of the author(s) and do not necessarily reflect the views of the National Science Foundation.

\section{Technical Evaluation}
\label{sec:technical-evaluation}

We have implemented our techniques in a tool, {\bf Strongarm}, that
is an extension of the OpenJML \cite{leavens_preliminary_2006,burdy_overview_2005}
program verification tool. Our tool will be part of a future OpenJML release.
In this section we evaluate the performance of our technique on the task of inferring specifications. In the next subsection we explain our experimental setup and provide specific details about the source code we conducted our experiments on. Following this, our evaluation looks at the performance of our technique from the following five perspectives:

\begin{enumerate}

  \item \textbf{Effectiveness of Inference} How many of the candidate methods we were able to infer?

  \item \textbf{Efficiency of Reduction} By how much were the specifications reduced?

  \item \textbf{Complexity of Inferred Specifications} Overly complex and overly simplistic specifications are not practical. What are the characteristics of the inferred specifications?

  \item \textbf{Performance of Inference Procedure} How well (with respect to time) did our technique perform at the task of inferring specifications?

  \item \textbf{Performance of Inferred Specifications} How effective is our technique at reducing specification nesting, decreasing specification length, decreasing prover execution time, and decreasing proof length?

\end{enumerate}

Finally, in Section \ref{ln:practical} we conclude with a human evaluation of the inferred specifications produced by our technique.

\subsection{Evaluation Methodology}
\label{sec:data-collection}

We designed a series of experiments designed to examine the effectiveness of our technique at inferring practical specifications. We selected a cross section of popular Java libraries: JUnit4 (JU4), JSON-Java (JJA), Commons-CSV (CSV), Commons-CLI (CLI), Commons-Codec (COD), Commons-Email (EMA), and Commons-IO (CIO).
The static characteristics of these libraries are summarized in Table~\ref{table:code}.

\renewcommand{\arraystretch}{1.1}
\begin{table}[h]
	\caption{Code metrics for APIs used in evaluation.}
	\label{table:code}
  \begin{tabularx}{\linewidth}{Xrrrr}
    \toprule
    API Name &  SLOC & Methods & Files & Version  \\ \toprule
    JUnit4 & 10,018 & 1,230 & 193 & 4.13\\
    JSON-Java & 3,201 & 200 & 18 & 20160212 \\
    Commons-CSV & 1,501 & 158 & 10 & 1.4 \\
    Commons-CLI & 2,666 & 194 & 22 & 1.3.1 \\
    Commons-Codec & 6,607 & 509 & 60 & 1.10\\
    Commons-Email & 2,734 & 192 & 22 & 1.4\\
    Commons-IO & 9,836 & 955 & 115 & 2.5 \\
    \midrule
    Total & \textbf{36,563} & \textbf{2,331} & \textbf{440} & -  \\
    \bottomrule
  \end{tabularx}
\end{table}

A method for inferring preconditions in large corpora was recently investigated in the work of Nguyen  et al. \cite{nguyen_mining_2014-1}. However, rather than specifying the preconditions for the methods in our study, we assume a vacuously true precondition, namely \lstinline!true!. Prior to construction of the final specification, the default precondition is removed and not tabulated in the final specification analysis. We do this so as to not simultaneously test the results of our work in parallel with the technique of Nguyen. As noted in Section \ref{sec:limitations}, we do not specifically attempt to infer invariants for loops and instead rely on user-written loop invariants. For the study presented in this paper loops were not annotated with such invariants. Additionally, our technique's inference technique assumes any field referenced in the body of a method should be visible in the inferred specification. However, in JML this is considered an error by default. For this reason, all private fields referenced in specifications have been given the special annotation \texttt{spec\_public} which allows private fields to appear in specifications. This promotion of private fields to \texttt{spec\_public} is performed automatically by our technique during inference and reflected in the inferred specifications; future work includes using JML features such as model fields to avoid declaring all fields to be \texttt{spec\_public}. Additionally, during our evaluation we discovered there were several methods we were unable to validate due to bugs in OpenJML; these methods were explicitly skipped in our evaluation.

Experiments were performed on the Stokes HPC cluster\footnote{https://arcc.ist.ucf.edu/index.php/resources/stokes/about-stokes} at the University of Central Florida. Each job node was configured with 6 Intel Xeon 64-bit processors, 42GB of RAM, and used Oracle JDK 1.8.0.131. Our technique produces extensive telemetry data as well as the inferred specifications. The results presented below are based on mining this telemetry data.

\subsubsection{Verification of Inferred Specifications}
\label{sec:ground-truth-constr}

Once a specification is inferred, we must have a standard way of knowing if the specification itself is correct. In our experiments we validated the inferred specifications in three different ways. First, in the creation of our technique, we built a comprehensive test suite consisting of approximately 100 hand-written and hand-verified test cases. Our tool passes this test suite. Second, once inferred specifications are produced, we use OpenJML's to type check the produced specifications. All of the specifications produced by our technique type check. Lastly, we use OpenJML's Extended Static Checker (with Z3 \cite{de2008z3} version 4.3.0).
70\% of the inferred specifications were verified by OpenJML.
In practice our technique would check these specifications before submitting them to a user and therefore would not produce an invalid specification. The cases we were unable to verify were caused by tool error or implementation issues in our technique. Verification in this fashion also checks for unsatisfiable clauses, which should not be present in practical specifications. In doing this, as noted in Section \ref{sec:limitations}, we do not consider the exceptional behavior of the method in question.

\subsubsection{Threats to Validity}
\label{sec:threats-validity}
As mentioned in Section \ref{sec:ground-truth-constr}, we use the OpenJML tool to check the results of our inferred specifications. A positive result from OpenJML certifies that the program code satisfies the given specification. This is an especially strong guarantee; since checking is done statically, this certifies that \textit{for all runs} (and potential input values) the specifications are valid. However, this depends on the soundness of the tool. This is a limitation in the following ways. First, OpenJML itself might have bugs and therefore might certify programs that are not correct. Second, the theory behind OpenJML itself might not be sound, i.e., it might admit incorrect programs (programs that do not satisfy their specification) under certain circumstances; however, it is believed that this second problem is limited to JML features with semantics that are not quite settled yet (such as details concerning invariants). Our study is not impacted by known problems in the semantics of JML. Lastly, in choosing JML as our target specification language, our approach to specification inference may not generalize to other specification languages as well as it has with JML. However, there are many Hoare-style specification languages that use pre- and postcondition specifications, such as Eiffel, and retargeting our technique to these specification languages should be a straightforward exercise for future work.

\subsection{Limitations}
\label{sec:limitations}
In designing our technique, we intentionally made some trade-offs to simplify its implementation. The two major limitations of our technique are seen in our handling of exceptions and in our handling of loop constructs. First, although JML allows for descriptions of exceptional method behavior, in our technique we do not attempt to infer this behavior (although information about the exceptional behavior of codes is present in our AST; it is simply elided). Instead this task is relegated to future work \cite{Dillig2013}. Second, as a simplifying assumption, in our implementation we assume that in the presence of loops that our technique will always have access to expert-written loop invariants. From these loop invariants we apply the standard Hoare loop rules to facilitate inferring postconditions.

\subsection{Effectiveness of Inference}
\label{sec:effect-infer}

For each of the libraries we categorized the status of an inference attempt in one of four different categories. We give an explanation of the categories in this section as well as provide some analysis of our findings; see Figure~\ref{fig:inference-breakdown}.

\begin{figure}[t]
  \centering
  \includegraphics[width=.8\linewidth]{figures/outcomes-barh}

  \caption{A summary of inference outcomes for our technique on our 7 test libraries. }
  \label{fig:inference-breakdown}
\end{figure}

The status \textit{Inferred} indicates that our technique successfully inferred a specification for a method. We define success as containing at least one postcondition in the form of an \texttt{ensures} or \texttt{assignable} clause (in the case a frame axiom is necessary). Other clauses may be (and often are) present. For all experiments our technique succeeded in producing a specification more than $74.0\%$ of the time (overall), and in its worst performance produced a specification $48.1\%$ (in Commons-CSV). Our technique's best success in producing specifications was on JUnit4 (92.5\%); this was largely due to JUnit4 having significantly smaller control flow graphs compared to other libraries. In our analysis we found that the CFGs for JUnit4 were less than 400 nodes, except for one case of 594 nodes.

\begin{figure}[t]
  \centering
\includegraphics[width=.8\linewidth]{figures/pct-reduction-barh}
\caption{A summary of specification length reduction for our technique on our 7 test libraries. }
\label{fig:reduction-breakdown}
\end{figure}

A status of \textit{Timeout} indicates that the inference process was aborted before inference could complete. For this paper we used a timeout of 300 seconds (5 minutes). We determined this timeout through repeated experimentation with different timeouts ranging up to 20 minutes. In our initial tests we determined that inference attempts that did not complete within 5 minutes were not able to complete in 20 minutes either. While higher settings for timeout timeouts might reduce the number of specifications that fail to be inferred, the combined timeout was only about $9\%$. When a timeout occurs the intermediate results are discarded and not included in our remaining analyses. In the results reported in Figure~ \ref{fig:inference-breakdown} we can see that the two worst performing subjects in terms of timeout are Commons-CSV ($51.3\%$) and JSON-Java ($23.0\%$). Unlike the other test candidates, both Commons-CSV and JSON-Java are both parsers that contain deeply nested code. In all other libraries timeout performance was excellent and perhaps these results suggest that inferring specifications for parsers, since they are inherently very recursive, is more difficult than inferring specifications for general purpose code.

A status of \textit{Refused} means that our technique did not attempt to infer a specification, because the control flow graph (CFG) size was larger than a preset limit (a CFG size of 500 nodes). Similar to the timeout parameter, larger CFGs typically take much longer to infer. In our evaluation a size of 500 proved to be a reasonable choice, since the number of refused methods represented only $3.9\%$ overall. This number is partially inflated by the unusually high number of refused methods in Commons-IO. This is explained by higher CFG complexity relative to the other libraries in the test suite. This additional complexity comes from the way the verification conditions for exceptional code are generated. Although we are not inferring the specifications for the exceptional specifications cases, the exceptional information exists in the CFG that our technique analyzes to infer the normal specification cases. Since Commons-IO deals with input/output related functions it has an unusually high number of exceptions. This greatly inflates the size of the CFG, which made fewer of its methods usable for our study. This effect could be mitigated if the exceptional nodes were removed from the CFG prior to inference but such a change would make it then impossible to later infer the exceptional behavior of methods.

A status of \textit{Error} means that our technique encountered an internal error during inference. We manually investigated these errors and found them to be generated from current limitations in OpenJML itself. For example, certain features, such as enumerated types, are not currently supported in OpenJML (although they are valid in JML itself). Our implementation is based on OpenJML 0.8.12; we expect to be able to reduce the amount of internal error our tool encounters as errors are corrected in OpenJML.

\subsection{Efficiency of Reduction}
\label{sec:efficiency-reduction}

\begin{figure}

  \centering
\includegraphics[width=\columnwidth]{figures/stick-graph-v2}

\caption{The initial and final specification length for all inferred specifications (all test libraries combined, binned to 262 equal width bins).  Light lines indicate length before applying our technique; dark lines show our technique's effect on length. In this paper we consider 1/4 page to be equal to 20 lines.}
\label{fig:red-blue}
\end{figure}

As discussed in Sections~ \ref{sec:introduction} and \ref{sec:technical-approach}, one of the problems impacting specification inference by symbolic execution (and therefore predicate transformers) is the length of the resulting inferred specification. In this section we will evaluate how effective our technique was at reducing the length of specifications inferred by symbolic execution.

In Figure~ \ref{fig:red-blue}, we show the length of the initial and final inferred specifications in terms of lines of specification. Additionally, since short specification length can be a desirable quality from a software engineering and readability perspective, we also provide two reference lines: one at one full page (80 lines) and one at a quarter page (20 lines). In our analysis, $95.0\%$ of specifications fell below one full page length and $84.6\%$ fell below one quarter page length. This suggests that our techniques for reducing specification size were effective in reducing the size of most of the inferred specifications.

The results in Figure \ref{fig:red-blue} give an overview of all inferred specifications. However, our technique's effectiveness at reducing the final specification length of individual code bases varied significantly. In Figure \ref{fig:reduction-breakdown}, we can see a breakdown of our technique's effectiveness at reducing the final size of inferred specifications. Of the most interest are 80-100\% category (the \textit{most} reduction), and the 20-40\% reduction category (the \textit{least} reduction). Although we created a category for it, none of the code bases contained specifications that were reduced in the 0-20\% category. In our experiment, we found that the 80-100\% category contained 41.6\% of all methods. In Figure \ref{fig:reduction-breakdown} we see that the worst performer (least reduction) was Commons-Email. We did further analysis of this phenomenon where we looked at the length of the methods being inferred, the control flow depth, and the resulting reduction classification. We did not manage to find a relationship between these variables, which may suggest that these contracts failed to reduce more significantly because they described essential (non-reducible) logical states rather than non-practical artifacts as described in Section \ref{sec:technical-approach}.

\subsection{Complexity of Inferred Specifications}
\label{sec:compl-inferr-spec}

Criticisms of prior work on specification inference have included that the inferred specifications were either too short and not descriptive enough or template based and not expressive enough to capture the meaning of programs not falling within the parameters of the templates. We examine complexity in three different ways. First, in Figure \ref{fig:red-blue} we give metrics on the variation in the length of specifications produced by our technique. To quantify the distribution of types of clauses our technique was able to infer, in Table \ref{table:complexity}, we report on the variation of clauses present in the specifications inferred by our technique for each of our target codebases. In Table \ref{table:complexity} we can see that inferred specifications were comprised of mostly \texttt{requires} clauses, followed by roughly 4 times less \texttt{ensures} clauses as well as smaller numbers of \texttt{pure} and \texttt{assignable} clauses. Our technique is able to handle quantifiers such as \texttt{forall}, however we did not examine its distribution in the inferred specifications.  In Figure \ref{fig:far-nesting}, we detail the specification case nesting present in the inferred specifications. This is discussed further in Section \ref{sec:far-performance}.

\renewcommand{\arraystretch}{1.1}
\begin{table}[t]
	\caption{Summary of JML clauses in inferred specifications.}
	\label{table:complexity}
  \begin{tabularx}{\linewidth}{Xrrrrrr}
    \toprule
    API &  Methods & \texttt{requires} & \texttt{ensures} & \texttt{assignable}  & \texttt{pure} \\ \midrule
    JU4         & 1,230  & 845   & 631 & 153  & 588 \\
    JJA     & 200   & 209   & 183 & 24   & 40  \\
    CSV   & 158   & 70    & 91  & 34   & 23  \\
    CLI   & 194   & 1,301  & 422 & 118  & 27  \\
    COD & 509   & 1,533  & 569 & 105  & 90  \\
    EMA & 192   & 7,139  & 622 & 191  & 47  \\
    CIO    & 955   & 1,483  & 681 & 270  & 641 \\
    \midrule
    Total & \textbf{2,331} & \textbf{12,580} & \textbf{3,199} &  \textbf{895} & \textbf{1,456}   \\
    \midrule
    Ratio & - & 5.39 & 1.37 & 0.38  & 0.62 \\

    \bottomrule
  \end{tabularx}
\end{table}

\subsection{Performance of Inference}
\label{sec:perf-infer-proc}

To better understand the runtime performance characteristics of our technique we collected telemetry data about its performance. In our analysis, we found that the data was tightly clustered  between $10^1$ and $10^2$ ms. Note that inference time in our experiment was limited to 5 minutes ($3 \times 10^5$ ms). Many of the observed data points fell within this region, suggesting a linear fit with the exception of some very large control flow graphs which fell in the region bordering the timeout. These data points were identified as belonging mostly to Commons-IO and due largely to the number of exceptional flows present in the resulting control flow graphs (see Section~ \ref{sec:effect-infer} for more details). As discussed in Section~ \ref{sec:effect-infer}, using the timeout threshold of 5 minutes with the current performance characteristics allowed us to infer more than 75\% of the methods we considered for this study with an average inference time of just 2 seconds per method.

\subsection{Performance of our technique}
\label{sec:far-performance}

\begin{figure}[h!]

    \centering
    \includegraphics[width=0.7\linewidth]{figures/nesting-bar}

  \caption{The effect of our technique on the nesting of inferred specifications }
  \label{fig:far-nesting}

\end{figure}

To better understand the performance of our technique with respect to more standard techniques such as removing tautologies, we conducted further evaluation to study our technique. We conducted our study by taking the same 7 libraries used throughout this section and examining the effect of running all of the standard analysis types (Section \ref{subsec:implementation-details})  with the exception of our technique in one run and all of the analysis types \textit{with} our technique added back into the analysis pipeline. To understand the characteristics of specifications before and after our technique is applied to them we observed 4 different metrics. The first metric we observed was \textbf{specification nesting}. Specification nesting is defined as the lexical depth of a specification. In Figure \ref{fig:far-nesting}, we present the performance of our technique in reducing nesting of specifications. In this case of all libraries, our technique achieved a reduction in nesting, producing an overall average reduction of 73.8\%.

In our examination of the \textbf{percent reduction} aspects of our technique, we found our technique's effect on specifications is not necessarily to produce large reductions in the length (as measured in lines) of specifications; our technique's contribution to the length (in lines) is small compared to the contribution of the other steps (our technique contributes an additional $\approx 10\%$ reduction overall).

Ultimately, for a specification to be most useful, it should be used to verify the implementation of the code it specifies. In Figure \ref{fig:far-proof-length}, we examine the impact of our technique on the \textbf{proof length}, i.e., the length of the SMT conditions generated that are needed to verify the correctness of a specification in relation to its implementation. In Figure \ref{fig:far-proof-length} we can see that our technique has a large impact on the size of the generated SMT proofs for the code samples we studied. Overall, \textit{our technique reduces the size of the generated SMT conditions by 76.7\%}.

\begin{figure}[t]

  \begin{subfigure}{.5\linewidth}
    \includegraphics[width=\linewidth]{figures/proof-length-far-vs-no-far}
  \caption{}
  \label{fig:far-proof-length}
  \end{subfigure
  \begin{subfigure}{.5\linewidth}
    \includegraphics[width=\linewidth]{figures/proof-time-far-vs-no-far}
  \caption{}
  \label{fig:far-proof-time}
  \end{subfigure}%

  \caption{The effect our technique on (a) the length of the SMT conditions generated from specifications (b) the time needed to check the inferred specifications.}
\end{figure}

In the previous paragraph we saw that our technique is effective for reducing the size of the proofs required to verify implementations of inferred specifications. To determine the impact of the reduced length on the time to run the SMT solver on these proofs, we studied the \textbf{solver times} with and without our technique. In Figure \ref{fig:far-proof-time} we show the time taken to prove the specifications inferred with and without our technique. As can be seen in all cases, our technique reduces the time taken to verify the SMT conditions. Across all libraries, our technique reduces the prover execution time by  26.7\%.

\section{Overview of Techniques for Inferring Specifications}
\label{sec:overview-of-execution-techniques}

(describe all the different types of execution models)

\section{Introduction}
\label{sec:introduction}

Frameworks and libraries are the basic building blocks of modern software,
using them via their application programming interfaces (APIs),
which are collections of classes and their methods.
A specification for an API method is a contract~\cite{Meyer88,burdy_overview_2005}.
An API method's {\em precondition} is a predicate
that must hold when it is called;
an API method's {\em postcondition} is a predicate that the method ensures will hold when it completes.
For instance, the
\texttt{push(item)} method of \texttt{java.util.Stack}
ensures that \texttt{item} is the top of the stack.

Knowledge of postconditions is very useful for automated software
engineering tools such as formal verification of
program correctness~\cite{Ammons02,ball-spin01,xie-popl05},
test case generation~\cite{dart-pldi05},
test oracle creation~\cite{tonella-fse13},
detecting bugs~\cite{engler-sosp01,prminer-fse05,weimer05},
design by contract~\cite{burdy_overview_2005,yiwei-icse11}, etc.
Popular formal specification
tools include ESC/Java~\cite{flanagan_extended_2002},
Bandera~\cite{bandera-icse00}, Java Path Finder~\cite{jpf},
JMLC~\cite{leavens_preliminary_2006}, Kiasan~\cite{kiasan-isola06}, Code
Contracts~\cite{codecontracts}, etc., regularly use postconditions
in place of a method call to gain scalability.

Unfortunately, pre- and postconditions specifications
are not widely available, even for widely-used
libraries. The main reason seems to be that the cost of writing such specifications
is similar to the cost of writing the code itself~\cite{Leavens-Clifton05a}.
To decrease the cost of writing specifications, several sets of techniques have
been proposed to automatically derive specifications.

A first set of techniques analyzes call sites of an API method
to collect a set of predicates at each of these call sites and then uses mining
techniques, such as frequent items mining, to infer preconditions
\cite{nguyen_mining_2014-1,Ramanathan07}.
Another body of work has focused on analyzing call sites to mine temporal patterns
over API method calls, e.g. \cite{Gruska-Wasylkowski-Zeller-10,Nguyen09,Wasylkowski07,Livshits05,Williams05,Michail00}.
However, these works do not infer postconditions.

A second set of techniques uses static analysis on the code
of the API method to infer specifications; e.g. Cousot {\em et al.} uses
abstract interpretation~\cite{Cousot2013} to infer preconditions,
and Buse {\em et al.} uses symbolic execution~\cite{Buse2008} to
infer conditions leading to exceptions.
However, Buse {\em et al.} do not infer conditions under which the API method
terminates normally and Cousot {\em et al.} do not infer postconditions.

A third set of techniques uses {\em dynamic} approaches to mining
specifications~\cite{Ammons02,Cousot2011,Dallmeier05,ernst_daikon_2007,Gabel08,Liu06,Lo09,Pradel09,Wei11,Yang06}.
Some of these works infer temporal patterns over API method calls~\cite{Yang06,Liu06,Gabel08,Lo09},
object-usage specifications~\cite{Pradel09},
and others
strengthen existing specifications~\cite{Wei11}.
Although Daikon~\cite{ernst_daikon_2007} can infer postconditions,
its inference depends on the presence of an adequate test suite~\cite{harder_improving_2003,nimmer_invariant_2002}.

\begin{figure*}[tp]

	\begin{subfigure}[t]{0.33\linewidth}
		\LSTJMLFILESLICE{10-26}{listings/cmp.java}
		\caption{A Java function \texttt{cmp}}
		\label{fig:cmp}
	\end{subfigure}
	\begin{subfigure}[t]{.335\linewidth}
		\LSTJMLFILESLICE{2-23}{listings/cmp-contract-pre.java}
		\caption{Postcondition of \texttt{cmp} using the standard SP}
		\label{fig:cmp-pre}
	\end{subfigure}
	\hspace*{\fill}
	\begin{subfigure}[t]{.33\linewidth}
		\LSTJMLFILESLICE{5-26}{listings/cmp-contract-post.java}
		\caption{Postcondition using our technique}
		\label{fig:cmp-post}
	\end{subfigure}
	\caption{The postcondition of \texttt{cmp} function obtained
	using the standard definition of SP is verbose, exposes implementation details,
	and is tied to the structure and flow of \texttt{cmp}.
	Our technique infers concise postconditions that eliminates
	those limitations.
}
    \label{fig:cmp-overall}

\end{figure*}

This paper proposes a technique for inferring postconditions that combines
forward symbolic execution~\cite{gordon_forward_2010} with predicate transformers~\cite{dijkstra_discipline_1997}.
Starting from a precondition (e.g., \lstinline!true! or one inferred
using prior techniques~\cite{nguyen_mining_2014-1,Ramanathan07})
our technique uses the body of the API method to produce a logical
formula that can be converted into a specification, as shown in Figure~\ref{fig:cmp-overall}.

To empirically evaluate our approach, we apply it to infer postconditions
for seven popular Java libraries: JUnit4 (JU4), JSON-Java (JJA), Commons-CSV (CSV), Commons-CLI (CLI), Commons-Codec (COD), Commons-Email (EMA), and Commons-IO (CIO)
totaling over 2300 methods.
Our results show that our technique has a very high precision and recall.
We were able to infer specifications for 75.7\% methods, and
all of the inferred specifications were verified to be correct using
OpenJML's Extended Static Checker (with Z3 \cite{de2008z3} version 4.3.0).
Our results show that our inferred specifications are both rich and concise.
To evaluate richness, we study the presence of \texttt{assignable} and
\texttt{purity} clauses (in addition to pre- and postconditions) in inferred
specifications. The purity clause documents whether an API method will change
memory locations, and the assignable clause documents which memory locations
can be changed.
We find that all the API methods with inferred specifications have either
a purity clause or an assignable clause.
To evaluate conciseness, we study the length of final specifications and find
that 84.6\% of inferred specifications are less than 1/4 page in length.

Our key contributions include:
\begin{enumerate}
	\item A novel technique for mitigating the effect of state space explosion in the context of inferring specifications using strongest postcondition predicate transformers.
	\item The implementation of a tool, {\bf Strongarm}, that
	embodies our postcondition inference technique as an extension of the OpenJML \cite{leavens_preliminary_2006,burdy_overview_2005} program
	verification tool. Our tool will be part of a future OpenJML release
	that will make our techniques available to formal methods community.
	\item A series of techniques and a novel, graph-based algorithm
	for producing concise specifications.
	\item An experimental evaluation of Strongarm on seven
	popular Java libraries that demonstrates its effectiveness.
	\item A benchmark of seven specified libraries.
\end{enumerate}

Next, we will motivate our approach.
Section~\ref{sec:our-approach} describes our approach,
Section \ref{sec:technical-evaluation} presents its evaluation,
Section \ref{sec:related-work} compares it with related work,
and Section \ref{sec:conclusion} concludes.

\section{Motivation}
\label{sec:motivating-example}

The standard technique for statically computing the postcondition for a piece of
code was formalized by Dijkstra in the form of the
\textit{strongest postcondition predicate transformer} \cite{dijkstra_discipline_1997}
(SP). SP is a functions that takes a predicate describing a starting
state (i.e., a pre-state) and a statement, and produces predicate that describes
the set of states that may result from executing that statement on any
pre-state that satisfies the given predicate.
Many researchers have used the opposite predicate transformer, the
weakest precondition transformer, also introduced by Dijkstra,
for building verification tools,
including ESC/Java, Boogie \cite{leino_this_2008}, OpenJML, and many others.
However, SP itself has not been previously leveraged for successful tools that infer
postconditions.

To understand reasons why SP has not been successfully used before,
consider inferring the postcondition of the Java function in Figure \ref{fig:cmp}.
Figure \ref{fig:cmp-pre} shows the results of applying SP on that
code, starting from the predicate \textbf{\texttt{true}},
and translating the resulting proposition to the JML notation.
The JML keyword normal\_behavior means that this specification is
about the normal termination.
As is usual in SP, conditions are accumulated as the tool traverses the control flow
of the function.
Since this function has three exits, this results in three alternative postconditions.
The syntax \{$\mid$~A~\texttt{\textbf{also}}~B~$\mid$\} means that the
implementation must obey both specifications $A$ and $B$,
or, equivalently, that a caller may conclude the postcondition of either $A$ or $B$.
Starting with the precondition of \textbf{\texttt{true}},
the first assignment leads to accumulation of the condition \texttt{c==a}.
The if-condition leads to accumulation of the condition \texttt{c<b} in the
true branch, and its negation \texttt{!(c<b)} in the false branch.
The first (lexical-order) return statement is an exit point, and
thus leads the postcondition \texttt{\textbackslash result} \texttt{==} \texttt{-1}.
Thus, at the first return statement we get four accumulated conditions.
\texttt{c<b} (from the if condition), \texttt{true} (from the precondition),
\texttt{\textbackslash result} \texttt{==} \texttt{-1} (from the
return), and \texttt{c==a} (from the assignment).
The second if statement (within the body of else) leads to accumulation of the
condition \texttt{c>b} in the true branch and its negation in the false branch.
The second return statement thus
leads to the postcondition \texttt{\textbackslash result} \texttt{==} \texttt{1},
along with
\texttt{!(c<b)} (from the first if), \texttt{(c>b)} (from the second if),
and \texttt{true} (from the precondition).
The third return statement is similar.

As the resulting postconditions show,
a straightforward use of the predicates produced by SP for
specification inference
leads to verbose results that: (1) expose the internal details of the function
such as internal variables (e.g., \texttt{c}) and assignments to such variables that are
not part of the interface,
(2) postconditions that are directly tied to the structure of the code
and its control flow, and
(3) significant redundancies that could increase the cost of reading and using
such specifications.

Figure \ref{fig:cmp-post} shows the postconditions produced by our approach
and previews its advantages.
These postconditions are in terms of function arguments,
reorganized to reduce redundancies, and eliminate internal
details and tautologies.

\subsection{A Study of the Inferred Specifications} \label{ln:practical}

To determine if the specifications produced by our technique were useful to human readers, we conducted a small study to examine their usefulness. In general, we believe that practical specifications are more useful for human readers than those that are not, since they tend to be shorter and more to the point. However, we defined additional criteria against which we designed our study.

Namely, we selected the following criteria and say that a specification is \textit{practical} if they:

\begin{itemize}
\item
do not contain redundant formulas,
\item
do not contain unsatisfiable formulas,
\item
do not contain tautological formulas,
\item
specify frame axioms \cite{Borgida:1993:LNE:257572.257636}),
\item
specify when a method is pure (has no side-effects),
and
\item
only use names that are visible to a method's clients.
\end{itemize}

\textbf{Methodology.} Using the specifications inferred by our technique, we conducted a survey of people familiar with the Java Modeling Language (JML)~\cite{leavens_preliminary_2006}. The survey used 12 pairs of method specifications inferred by our technique; to highlight the aspects of our definition of practical specifications, one element of each pair had one aspect, e.g., removal or unsatisfiable formulas, disabled.
The survey was completed by 25 people, 18 of which said that they ``definitely'' had experience reading JML and 7 of which had some experience with JML.  All correctly answered a simple question about JML that tested their understanding of a method specification with two specification cases.
(A method \emph{specification case} in JML is a pre- and postcondition specification, with optional frame axioms, that must be satisfied whenever the case's precondition is true when the method is called.)
The questions in the survey were all simplifications of pairs of output given by our tool, one of which was not processed to remove a single impractical feature (according to the above definition).

\textbf{Results.} An unsatisfiable precondition, such as \lstinline/!true/, causes the specification case it appears in to be useless.
87.5\% of the survey respondents preferred a specification without unsatisfiable preconditions, including preconditions that required non-null fields to be null.
Another example of unsatisfiable specifications comes when a specification case has two mutually-contradictory clauses; in this case all
respondents preferred a specification without such unsatisfiable combinations of clauses (75\% of them strongly so).

According to the survey, 95\% of the respondents preferred a specification without the tautological postcondition \lstinline!true == true!.
Also, 62.5\% of the respondents preferred a specification without tautologies such as \lstinline!requires true! and more subtle tautologies involving non-null declarations. Another 87.5\% preferred a specification without subtle redundancies such as \lstinline/"No resource defined" != null/.
In another question, 80\% of the respondents preferred a specification without redundant clauses requiring non-null fields to be not null.
In another question, 93.3\% of the respondents preferred a specification without duplicated specification cases.

Regarding frame axioms, the survey contrasted a specification
without the frame \lstinline!assignable this.name!
with a nearly identical specification with the assignable clause.
Although the specification without the frame axiom is shorter, 86.7\% of the respondents preferred the specification with the frame axiom (53\% strongly so).

In JML a pure method is one without any side-effects, and is specified by the \lstinline!pure! keyword. The \lstinline!pure! keyword also functions as a strong frame axiom.
66.7\% of the respondents preferred a specification to one just like it but without the keyword \lstinline!pure!.

In sum, the majority of the survey respondents preferred specifications that satisfy our notion of a ``practical'' specification (the kind our technique produces), even if the differences were rather subtle.

\subsubsection{Translation of $SP$ and JML Specifications}
\label{sec:jml-to-prop}

In this section we discuss the translation semantics for translating JML specifications to and from the propositional form. We give a listing of our translation semantics in Figures \ref{fig:jml-to-prop} and \ref{fig:prop-to-jml}.

As mentioned in Section \ref{sec:specs-as-boolean-formulas}, one of the important aspects of our approach to performing JML specification translation is that we treat the individual statements of the specification as opaque, i.e., we do not consider the meaning of the expression contained within a \textbf{\texttt{requires}} statement. Rather, we treat them as opaque propositions to be translated. This impacts our translation semantics and necessitates the creation of a variable store which will keep track of these associations. We define a variable store, $V$ as follows:
\begin{equation}
V = \{[x \mapsto v]\}
\label{eqn:v-defn}
\end{equation}

For each of the members of the semantic class \clz{JMLClauseExpr} we define two forms of the translation function. The first form, e.g., \textsc{TR-Req-1}, converts the given \clz{JMLClauseExpr} to an opaque variable and requires that the expression has been previously converted. The opaque variable that is used is reused from the previous association of the expression within the variable store. The second form, e.g., \textsc{TR-Req-2}, does not require that the given \clz{JMLClauseExpr} has been previously defined. Instead it associates a fresh variable name with the given expression in the variable store.

Additionally, in our translation semantics we make use of a special notation:

\begin{equation}
  \sigma \thicksim \mathit{expr}
\end{equation}

The meaning of this notation is that $\sigma$ acts as a synonym for $\mathit{expr}$ and it is used in the translation rules that require the use of the variable store $V$.

redpajama_set_name: RedPajamaArXiv


By definition, a phobia is an extreme fear of something. Sometimes this fear goes beyond what people would consider normal logic. The list of phobias that people experience on a daily basis is endless. Some are scared of heights, germs, enclosed spaces, dark areas, and spiders. Others are fearful of clowns, going outside, and flying. No matter what the fear stems from, the fact remains that it can cause some people a great deal of stress and anxiety.
Although it may feel hopeless when confronted with that fear, it is still possible to conquer your phobia. In order to do so, you will have to evaluate yourself, learn more about your fear, and possibly even put yourself in a few uncomfortable situations.
Sometimes the key to overcoming the fear of something is to learn more about it. In the process of educating yourself, take a moment to learn not only about the phobia but also find out more about the object or situation that scares you. For example if you have a deathly fear of snakes, try to find out more information about other people that also have snake phobias. Take it one step further and start learning more about snakes themselves. You may find that the more you learn about them, the less you fear them.
Learning about your actual phobia will allow you to see if there are any existing support groups or information available to help you overcome your fear. You can also search for any available solutions that you may not have tried yet.
Learning more about the object of your fear can help you to dispel any myths or falsehoods that you may have previously believed. In the course of educating yourself, you may find that you feared situations or behaviors that are not even possible or very unlikely to occur.
Ultimately, educating yourself will let you know if your fear is justified, and if so, what you can do to help lessen it in the future.
One of the first things to try when attempting to overcome a fear is to find out exactly why and when it began. A lot of phobias are the result of negative past experiences, and as time goes on the event gets forgotten but the anxiety remains.
What was it about the situation that made you feel so anxious?
Would this same situation scare you today, or were you just not able to fully process it at the time?
Was there any way you could have taken control of the situation? Would you be able to take control of that situation today?
After asking yourself these questions, you may find that a lot of the mystery surrounding your phobia is gone. Facing your fear on a daily basis may become a little bit easier once you establish exactly where it came from. On the flip side, your answers could end up causing you more distress once you know the true cause of your fear. If this is the case, you may need to consult a doctor or counselor for further help.
Do you remember the exact moment your greatest fear began?
One of the best ways to work on getting over any type of fear is to confront it. Although initially it may cause a great deal of anxiety, eventually you may find yourself at a point where it does not stress you out as much.
A person's comfort zone is usually made up of the people, activities, and experiences that someone is used to seeing on a regular basis without feeling anxiety. Anything that causes fear or an immense amount of stress normally falls outside of that zone. As you recognize your own phobias, you begin to move any activities related to them outside of your comfort zone in order to avoid them.
However by purposefully confronting your fear, you can slowly cause your comfort zone to expand. Eventually things that used to scare you will become more routine and bearable. As the behaviors become more routine, the stress related to them will also start to disappear. Over time, you may notice that your comfort zone has expanded to the point that you no longer have your phobia.
Sometimes people are able to get over hardships faster when they realize they are not in the struggle by themselves. Having other people to talk to and lean on can make dealing with a phobia more bearable.
In these situations, there are often support groups available for people experiencing specific phobias. These groups may meet face to face or take place as online forums. No matter what the format is, they allow people in similar situations to discuss the issues they are facing.
They allow you to meet others dealing with the same phobia. They also give you strength knowing you are not the only one going through the ordeal.
They give you a chance to verbalize what your experience is like. Talking about your problem with others may help to relieve some of the anxiety that has built up inside.
They may help you to identify exactly when your phobia starts to occur, and what types of feelings you experience when it does occur. By learning what your "warning signs" are, the doctor can work with you on developing coping techniques to minimize the amount of stress you feel.
For those struggling to adjust their response on their own, the doctor may also be able to prescribe medication to lessen the amount of anxiety a person feels. While this may not allow you to completely conquer a phobia, it can enable you to function at a higher level when faced with one.
Dealing with fear is as much about how you respond to certain situations as it is about what is causing them. Although it may be difficult to try overcoming them, phobias can be conquered. With the right attitude, support from others, and knowledge of your phobia, you can make an overwhelming sense of fear a lot more tolerable.
"Specific Phobias". Anxiety and Depression Association of America. Retrieved August 26, 2017.
Grohol, John M. (May 17, 2016). "Overcoming Fears, Phobias, and Panic Attacks". PsychCentral. Retrieved August 26, 2017.
Lewis, Dyani (August 16, 2017). "Adult Brain's Fear HQ Can Grow New Cells". Cosmos. Retrieved August 26, 2017.
Thomas, Liji (July 20, 2017). "Treatment Options for Social Anxiety". News-Medical.net. Retrieved August 26. 2017.
"Start a Support Group". Anxiety and Depression Association of America. Retrieved August 26, 2017.


Along with our friends at St. Charles and Catholic Central, we gathered for prayer and then went in all directions in support of Love, Inc and the Transitional Living Center! St. Mary families donated $2140 and had over 300 walkers. Nice job!


text:
Shweta Tripathi, Ali Fazal celebrate wrap up of 'Mirzapur 3' in Goa
Shweta mentioned, "I couldn't wait to start shoot as soon as we got the episodes for season 3.
Shweta Tripathi Sharma Instagram
3 Dec, 2022, 4:34 am
MUMBAI: Shweta Tripathi Sharma never fails to stun the audiences with her powerful portrayals. One such portrayal is by the actor, Gajgamini aka Golu Gupta from the 'Mirzapur'.
On Friday, Shweta completed shooting for season 3 of 'Mirzapur' and shared an emotional note.
Celebrating the wrap of season 3 of Mirzapur, Shweta took to Instagram and shared a reel video pouring her heart out, celebrating her sweet moments with the cast and crew, capturing how much goes behind camouflaging into a character and imbibing it in spirit.
A post shared by Shweta Tripathi Sharma (@battatawada)
When you come back to set to shoot for Mirzapur, it's a responsibility (which we are very happy to have) because of the unconditional love and unending cheer we get from the audience and we never want to let them down.
And now that we have completed shoot, I can't wait for all of you to see it, to experience what we have in store for you! It's been one hell of a challenging and a fulfilling ride. She's one of the bravest, toughest and most endearing girls I've met. And this cast and crew and the biggest gems."
Fans have been consistently citing their excitement for the release, demanding an official announcement of the release date. As the wrap up has been announced, season 3 of one of the most loved web series franchises shall move to post-production.
'Mirzapur' is the story of Kaleen Bhaiyya, the King Of Mirzapur vs the Pandit Brothers, Guddu, and Bablu. What initially begins as a battle for power, leading to the throne of Mirzapur, eventually shapes the destiny of the city, influencing its business and its politics. The web series was released on November 16, 2018.
Appreciated by fans and critics alike for its gripping storyline and phenomenal performances, the previous season of 'Mirzapur' had taken the unmatched fandom of the show several notches higher.
The second season not only recorded one of the highest completion rates but remarkably almost half of the viewers who completed the series, binge-watched the second season within just 48 hours of its launch, setting a new benchmark.
With an ensemble cast featuring Pankaj Tripathi, Ali Fazal, Divyenndu Sharma, Rasika Dugal, Harshita Shekhar Gaur, Vikrant Massey in the lead roles, the show continues to receive massive appreciation and viewership from across the world.
Actor Pankaj Tripathi
Shweta Tripathi Sharma
Kaleen Bhaiyya
King Of Mirzapur
powerful portrayals

redpajama_set_name: RedPajamaCommonCrawl


text:
The new Olympus digital PEN is called the E-P1
Olympus E-P1
Well, it's not a teaser anymore, and Olympus has officially announced its new micro FourThirds (mFT) DSLR is the E-P1.
The Olympus E-P1 is "NOT A POINT & SHOOT. NOT AN SLR. IT'S A PEN." The first PEN camera was introduced in 1959 and last PEN camera was the PenFT, introduced in 1966. Olympus is therefore celebrating the 50th Anniversary of the first PEN camera with the introduction of the digital version of the PEN, the E-P1. The "E" positions it as in the same league as the Olympus E-Series DSLRs, the "P" denotes it as a "Pen" and the "1" is a promise of more to come. Sweet!
The Olympus E-P1 is a beautiful camera in a stainless steel body. It comes as silver (with black accents) or white (with a really retro beige/tan accents). It is Olympus' first mFT "mirror-less" DSLR with all the features enthusiasts are looking for. The E-P1 makes available the image quality obtained from a DSLR (its image sensor has the same size as the one in the E-30 and E-620) in a compact and light body made possible by the mFT mount. Plus, it keeps all the convenient features found in compact digicams, making it an ideal street camera.
Olympus PEN F and the new E-P1 side by side
The E-P1 features 12.3MP resolution (on a 17.3 mm (H) x 13.0 mm (V) High speed Live MOS Sensor), Sensor-shift Image Stabilization, Dust reduction, HD Movie 1280×720 with stereo sound (with activable or continuous AF), an extra large 3.0-in. LCD (230K dots), PASM modes, Scene Modes, Shutter speed range of 60 – 1/4000 sec., plus Bulb (up to 30 min.), Continuous Shooting at 3fps, RAW file format, hot shoe, Face Detection, Intelligent AUTO (auto scene recognition), Shadow Adjustment Technology, Digital Level, MF Assist. In a welcomed change, the E-P1 uses the Secure Digital (SD / SDHC) memory cards.
Four potential (and surprising) gotchas: there is no built-in flash (and the optional FL-14 is fixed pointing straight forward, so no bounce flash), there is no AF Illuminator, the LCD resolution is only 230K dots, and the metal tripod mount is not centered and inline with the lens.
The Olympus E-P1 will be available in July 2009 at a street price of CAD $849.99 (body only). For a mere $50 extra (CAD $899.99), most buyers would opt for the body plus the ED 14-42mm (28-84mm equiv.) f3.5/5.6 Zuiko Digital Zoom Lens. For CAD $999.99, you'll get the body plus a 17mm (34mm equiv.) f2.8 lens and the clip-on optical viewfinder.
The Olympus E-P1 is currently the smallest "DSLR", being even smaller than the E-450.
– Check out the Olympus Pen history, celebrating its 50th Anniversary.
– See Olympus Pen mFT Teaser
– TV Commercial
– OLYMPUS PEN E-P1 Product Information
– Press Release
– OLYMPUS PEN E-P1 QuickFact Sheet
– Visual History of the Olympus PEN
dil interchangeable lens system micro four thirds olympus olympus digital pen olympus e-p1
Introducing the Olympus E-P1
Lenses • Olympus
Olympus M.Zuiko Digital Lens Roadmap (as of November 27, 2019) Includes...
Cameras • Olympus
Olympus OM-D E-M5 Mark III: Compact & Lightweight, 20-MP Fast Live...
Olympus • Press Releases
Olympus + CreativeLive: 'Step Outside' – a Photo Event...
Olympus M.Zuiko Digital 2x Teleconverter MC-20 Doubles the Master...
Cameras • Firmware Updates • Olympus
Olympus Firmware Upgrades (June 19, 2019) for Mirrorless Cameras OM-D E-M1...
Firmware Updates • Olympus
The Latest Olympus Firmware Update (Mar. 7, 2019) for OM-D E-M10 Mark II...
Olympus TOUGH TG-6 is a Compact Camera Perfect for Rugged and Underwater...
Cameras • Panasonic
Panasonic Lumix G95 Micro Four Thirds Mirrorless Camera: 20MP Sensor, Fast...
Olympus Firmware Updates (Jan. 24, 2019) for Cameras E-M1 Mark II (Ver. 2...
Olympus M.Zuiko Digital ED 12-200mm F3.5-6.3 (35mm Equivalent 24-400mm)...
Olympus OM-D E-M1X Micro Four Thirds Mirrorless Camera: Integrated...
In Commemoration of Olympus' 100th Anniversary, 2000 Units of OM-D E-M1...
Olympus Develops M.Zuiko Digital ED 150-400mm (300-800mm, 35mm equivalent)...
Olympus M.Zuiko Lens Roadmap (as of January 2019)
Accessories • Olympus
Olympus Announces Flash System Designed for Wireless Radiowave Shooting:...
Firmware Updates • Olympus • Panasonic
Certain Olympus Micro Four Thirds Mirrorless Cameras (OM-D Series and Pen...
Olympus • Teasers
Olympus OM-D E-M1X Video Teaser #3
Olympus Will Celebrate Its 100th Anniversary: 1919 – 2019
Olympus Teases New OM-D E-M1X Micro Four Thirds Mirrorless to Be...
Cameras • Leica
Leica D-Lux 7 Compact Camera: Fast F1.7 3x Optical Zoom Lens, Four Thirds...
Olympus 8 x 42 PRO and 10 x 42 PRO High Performance Binoculars for Nature...
Olympus Perspective Playground, an Art Exhibition with Interactive and...
Editorial • Olympus • Panasonic
Micro Four Thirds: 10th Anniversary. Where to from here on?


text:
The many masks of modern art
By Theodore F. Wolff
The seeds of the mature style of many modernist artists can be found in their early work. Thus, Miro's famous, free-floating ''abstract'' forms were already hinted at in his youthful, ornamental landscapes and figure studies. And Pollock's swirling ''dribblings'' were forecast in his turbulent pre-Abstract Expressionist compositions.
The same holds true of Mondrian's right angles and primary colors, Matisse's formal simplifications, and Diebenkorn's elegant reductions. In each case, the artist's mature style evolved logically and inevitably from stylistic and conceptual seeds planted early in his career.
This was particularly true of several American painters of the 1930s whose styles changed or evolved dramatically during the late 1940s and early '50s. Stuart Davis, Ben Shahn, Willem de Kooning, Adolph Gottlieb, Mark Rothko - to mention only a few of the most noteworthy - simplified and ''streamlined'' their art to the point where it often seemed at odds with what it had been before. And even such painters as Milton Avery, Edward Hopper, and Charles Burchfield brought their art to a greater degree of formal simplicity during those years.
If artists weren't simplifying their art, they were boiling it down to what they felt were its absolute essentials. Pollock discarded the easel and brush for dribbling and hurling paint onto canvas laid out on the floor. Kline found his final style by isolating and magnifying a tiny segment of a drawing. And Guston went from complex figure paintings to canvases filled with sensitively attuned touches of pure color.
Modernism was in the air, and with it came painterly enthusiasm and one or another form of abstraction. Hardly anyone was immune. Those who tried to hold out were overwhelmed and soon forgotten. Within a few short years American painting had reversed itself. From being militantly conservative, it had moved to the position of the extreme avant-garde.
In retrospect, it seems logical that such artists as Rothko and Gottlieb should have made that leap toward abstraction. They were, after all, already quite close to a form of abstraction in their earlier work - representational though it might have been in theory. What is not so easily explained is why a few equally excellent and forward-looking painters of the 1930s did not make that leap, and continued on in the style they had forged during their youth.
A prime example is Joseph Solman, an American-scene painter of modernist tendencies who had worked for the WPA Federal Art Project from 1935 to 1941. His warm, richly colored, and beautifully designed street and harbor scenes were not only deeply felt, they were also among the most innovatively ''modern'' American paintings of the period.
Solman belonged to ''The Ten,'' an important vanguard art movement founded in 1935 to ''attempt to combine a social consciousness with an Abstract Expressionistic heritage, thus saving art from being mere propaganda on the one hand, or mere formalism on the other.'' ''The Ten,'' to which Gottlieb, Rothko, and Bolotowsky also belonged, was firmly opposed to the sentimental and romanticized Regionalism espoused by the likes of Curry and Wood, and tried to make its point first by refusing to exhibit at the Whitney Museum, and then by exhibiting independently as a group.
Its goal was to bring American art into the modernist mainstream without, at the same time, depriving it of its uniquely American flavor. ''The Ten'' were not, however, held together by theory or dogma, but by shared enthusiasms and a common goal. But even those were personalized by each of its members - and understandably so, for each was a painter first, and a theorist second. What they did have in common was a vision of painting that was loosely Expressionistic, that looked to Matisse, Picasso, Soutine, Rouault, and Ryder for formal guidance, and to the American scene for subject and inspiration.
Solman's art, in particular, represented a perfect balance between a strictly American subject - the streets and people of New York - and a very modernist way of painting that subject. His canvases of the 1930s were extraordinary evocations of very particular places ''Union Square,'' ''East Side Playground,'' and superbly orchestrated exercises in modernist form, composition, and color. Each was authentically ''New York,'' and provocatively ''modern'' at one and the same time.
It seems a bit surprising, therefore, that Solman didn't move on to become one of the American avant-garde of the 1940s, or, more precisely, one of that decade's important Abstract Expressionists. He certainly had the talent and the material for it. His paintings of the 1930s were among the best American paintings of the period. And, just as much to the point, they seemed only one step away from abstraction, and only another half-step away from a warm and sumptuous form of Abstract Expressionism.
Had he taken that step, I suspect he would have ranked among the very best of the Abstract Expressionists. But he did not, and his reasons for not doing so intrigue and fascinate me.
I asked the artist himself, and received a simple response: ''There were still too many aspects of the universe I wanted to paint.''
It was a good answer, and one that satisfied me. Art for him, in other words, was an act of exploration and discovery. It was an engagement, having a painterly dialogue between a specific place and its pictorial potential, and not the personification of an abstract theory or idea.
Solman painted in order to discover fascinating shapes and colors in the world around him, and to enrich his life by evoking them on canvas or paper. Since reality and art were so deeply intertwined for him, he could no more have denied the former for a total immersion in abstract color and form than he could have discarded the nourishment of food in order to savor more totally its flavor and taste.
All that makes great sense - except possibly to those who feel art must always evolve toward its logical conclusion. Who feel that a young artist who composes in severely geometric patterns cannot be truly himself until his art consists of nothing but circles, squares, and triangles. And that a youthful colorist won't become himself until his art consists of nothing but touches of pure color.
I'm grateful for the art of Joseph Solman. Not only because it is beautiful in itself, but because it reminds us that the best art isn't necessarily the most extreme.
'Fierce Poise' illuminates the career of an overlooked abstract expressionist
Lee Krasner: abstract expressionist painter in her own right
Alexander Calder upended the seriousness of art