Package: POAnnotation

POAnnotation

Coverage

1: /*******************************************************************************
2: *
3: *        Copyright (c) 2019 Nick Battle.
4: *
5: *        Author: Nick Battle
6: *
7: *        This file is part of Overture
8: *
9: ******************************************************************************/
10:
11: package org.overture.pog.annotations;
12:
13: import org.overture.ast.definitions.PDefinition;
14: import org.overture.ast.definitions.SClassDefinition;
15: import org.overture.ast.expressions.PExp;
16: import org.overture.ast.modules.AModuleModules;
17: import org.overture.ast.statements.PStm;
18: import org.overture.pog.pub.IPOContextStack;
19: import org.overture.pog.pub.IProofObligationList;
20:
21: public interface POAnnotation
22: {
23:         public IProofObligationList poBefore(PDefinition node, IPOContextStack question);
24:         public IProofObligationList poBefore(PExp node, IPOContextStack question);
25:         public IProofObligationList poBefore(PStm node, IPOContextStack question);
26:         public IProofObligationList poBefore(AModuleModules node, IPOContextStack question);
27:         public IProofObligationList poBefore(SClassDefinition node, IPOContextStack question);
28:
29:         public void poAfter(PDefinition node, IProofObligationList list, IPOContextStack question);
30:         public void poAfter(PExp node, IProofObligationList list, IPOContextStack question);
31:         public void poAfter(PStm node, IProofObligationList list, IPOContextStack question);
32:         public void poAfter(AModuleModules node, IProofObligationList list, IPOContextStack question);
33:         public void poAfter(SClassDefinition node, IProofObligationList list, IPOContextStack question);
34: }