Stack


1   /*
2   * JBoss, Home of Professional Open Source
3   * Copyright 2005, JBoss Inc., and individual contributors as indicated
4   * by the @authors tag. See the copyright.txt in the distribution for a
5   * full listing of individual contributors.
6   *
7   * This is free software; you can redistribute it and/or modify it
8   * under the terms of the GNU Lesser General Public License as
9   * published by the Free Software Foundation; either version 2.1 of
10  * the License, or (at your option) any later version.
11  *
12  * This software is distributed in the hope that it will be useful,
13  * but WITHOUT ANY WARRANTY; without even the implied warranty of
14  * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the GNU
15  * Lesser General Public License for more details.
16  *
17  * You should have received a copy of the GNU Lesser General Public
18  * License along with this software; if not, write to the Free
19  * Software Foundation, Inc., 51 Franklin St, Fifth Floor, Boston, MA
20  * 02110-1301 USA, or see the FSF site: http://www.fsf.org.
21  */
22  package test.dbc.stack;
23  
24  /**
25   *
26   * @author <a HREF="mailto:kabir.khan@jboss.org">Kabir Khan</a>
27   * @version $Revision: 37406 $
28   */
29  @org.jboss.aspects.dbc.Dbc
30  @org.jboss.aspects.dbc.Invariant ({"!$tgt.isEmpty() implies $tgt.top() != null","$tgt.isEmpty() implies $tgt.elements.size() == 0"})
31  public interface Stack
32  {
33     @org.jboss.aspects.dbc.PreCond ({"$0 != null"})
34     @org.jboss.aspects.dbc.PostCond ({"!$tgt.isEmpty()", "$tgt.top() == $0"})
35     void push(Object   o);
36  
37     @org.jboss.aspects.dbc.PreCond ({"!$tgt.isEmpty()"})
38     Object   pop();
39  
40     @org.jboss.aspects.dbc.PreCond ({"!$tgt.isEmpty()"})
41     Object   top();
42  
43     boolean isEmpty();
44  }
45  
46
A to Z: JavaDoc & Examples Daily Java News & Articles Open Source Projects Open Source Codes Free Computer Books Remove Frame
Popular Tags