Projects >> MEPK >>3fdcddf7afb4c015e4b2f46a371fc7fad1bb2ee9

Chunk
Conflicting content 
import java.util.Set;

<<<<<<< HEAD:src/mepk/TrustedProof.java
import mepk.internal.ParProof;
import mepk.internal.SeqProof;
import mepk.internal.TrivialProof;
=======
import mepk.builtin.internal.ParProof;
import mepk.builtin.internal.SeqProof;
import mepk.builtin.internal.TrivialProof;
import mepk.kernel.Justification;
import mepk.kernel.Proof;
import mepk.kernel.Statement;
>>>>>>> 5a9a11027387c369db72d4295e47613bd257a31a:src/mepk/builtin/TrustedProof.java

/**
 * A trusted proof is a {@link Proof} which is built on the trusted kernel.
Solution content 
import java.util.Set;

import mepk.builtin.internal.ParProof;
import mepk.builtin.internal.SeqProof;
import mepk.builtin.internal.TrivialProof;
import mepk.kernel.Justification;
import mepk.kernel.Proof;
import mepk.kernel.Statement;

/**
 * A trusted proof is a {@link Proof} which is built on the trusted kernel.
File
TrustedProof.java
Developer's decision
Version 2
Kind of conflict
Import
Chunk
Conflicting content 
 * the static methods in this class.
 */
public final class ProofStep extends Proof {
<<<<<<< HEAD:src/mepk/ProofStep.java

	private static final class TrivialProof extends Proof {

		private final Set statements;

		public TrivialProof(Set statements) {
			this.statements = statements;
		}

		@Override
		public Set getGrounding() {
			return statements;
		}

		@Override
		public Set getGrounded() {
			return getGrounding();
		}

		@Override
		public Justification getJustificationFor(Statement statement) {
			return null;
		}

	}
=======
>>>>>>> 5a9a11027387c369db72d4295e47613bd257a31a:src/mepk/kernel/ProofStep.java

	/** An internal version of a {@link ProofStep}. */
	public interface Internal {
Solution content 
 * the static methods in this class.
 */
public final class ProofStep extends Proof {

	private static final class TrivialProof extends Proof {

		private final Set statements;

		public TrivialProof(Set statements) {
			this.statements = statements;
		}

		@Override
		public Set getGrounding() {
			return statements;
		}

		@Override
		public Set getGrounded() {
			return getGrounding();
		}

		@Override
		public Justification getJustificationFor(Statement statement) {
			return null;
		}

	}

	/** An internal version of a {@link ProofStep}. */
	public interface Internal {
File
ProofStep.java
Developer's decision
Version 1
Kind of conflict
Class declaration
Chunk
Conflicting content 
	 * @return the grounded statement
	 */
	public Statement getGrounded1() {
<<<<<<< HEAD:src/mepk/ProofStep.java
		return internalProofStep.getGrounded1();
	}

	@Override
	public Set getGrounded() {
		return Collections.singleton(getGrounded1());
	}

	@Override
	public Justification getJustificationFor(Statement statement) {
		return new Justification(this, new TrivialProof(getGrounding()));
=======
		return internalProofStep.getGrounded();
>>>>>>> 5a9a11027387c369db72d4295e47613bd257a31a:src/mepk/kernel/ProofStep.java
	}

	@Override
Solution content 
	 * @return the grounded statement
	 */
	public Statement getGrounded1() {
		return internalProofStep.getGrounded1();
	}

	@Override
	public Set getGrounded() {
		return Collections.singleton(getGrounded1());
	}

	@Override
	public Justification getJustificationFor(Statement statement) {
		return new Justification(this, new TrivialProof(getGrounding()));
	}

}
File
ProofStep.java
Developer's decision
Version 1
Kind of conflict
Annotation
Method declaration
Method invocation
Method signature
Return statement
Chunk
Conflicting content 
	public void test1() {
		Statement s = Stat(Arrays.asList(Expression.Type("P", "bool"), Var("P")), Var("P"));
		ProofStep p = ProofStep.Substitute(s, "P", Var("Q"), Types.EmptyMap());
<<<<<<< HEAD
		Statement expected = Stat(Arrays.asList(Expression.Type("Q", "bool"), Var("Q")), Var("Q"));
		assertEquals(expected, p.getGrounded1());
=======
		Set expected = Collections.singleton(Stat(Arrays.asList(Expression.Type("Q", "bool"), Var("Q")), Var("Q")));
		assertEquals(expected, p.getGrounded());
>>>>>>> 5a9a11027387c369db72d4295e47613bd257a31a
	}

	@Test
Solution content 
	public void test1() {
		Statement s = Stat(Arrays.asList(Expression.Type("P", "bool"), Var("P")), Var("P"));
		ProofStep p = ProofStep.Substitute(s, "P", Var("Q"), Types.EmptyMap());
		Statement expected = Stat(Arrays.asList(Expression.Type("Q", "bool"), Var("Q")), Var("Q"));
		assertEquals(expected, p.getGrounded1());
	}

	@Test
File
Test1.java
Developer's decision
Version 1
Kind of conflict
Method invocation
Variable
Chunk
Conflicting content 
		ProofStep p = ProofStep.Substitute(s, "P", AppV("and", "Q", "R"), Types.map("Q", "bool").map("R", "bool"));
		Set expected = Collections.singleton(Stat(
				Arrays.asList(Expression.Type("Q", "bool"), Expression.Type("R", "bool"),
<<<<<<< HEAD
						Expression.Type(AppV("and", "Q", "R"), "bool"), AppV("and", "Q", "R")), AppV("and", "Q", "R"));
		assertEquals(expected, p.getGrounded1());
=======
						Expression.Type(AppV("and", "Q", "R"), "bool"), AppV("and", "Q", "R")), AppV("and", "Q", "R")));
		assertEquals(expected, p.getGrounded());
>>>>>>> 5a9a11027387c369db72d4295e47613bd257a31a
	}

	@Test
Solution content 
		ProofStep p = ProofStep.Substitute(s, "P", AppV("and", "Q", "R"), Types.map("Q", "bool").map("R", "bool"));
		Statement expected = Stat(
				Arrays.asList(Expression.Type("Q", "bool"), Expression.Type("R", "bool"),
						Expression.Type(AppV("and", "Q", "R"), "bool"), AppV("and", "Q", "R")), AppV("and", "Q", "R"));
		assertEquals(expected, p.getGrounded1());
	}

	@Test
File
Test1.java
Developer's decision
Version 1
Kind of conflict
Method invocation
Chunk
Conflicting content 
		ProofStep w = ProofStep.Weaken(sp, DVRSet.EMPTY, Expression.Type("Q", "bool"), Var("Q"));

		assertEquals(Collections.singleton(sp), w.getGrounding());
<<<<<<< HEAD
		assertEquals(spq, w.getGrounded1());
=======
>>>>>>> 5a9a11027387c369db72d4295e47613bd257a31a
		assertEquals(Collections.singleton(spq), w.getGrounded());

		w.verify();
Solution content 
		ProofStep w = ProofStep.Weaken(sp, DVRSet.EMPTY, Expression.Type("Q", "bool"), Var("Q"));

		assertEquals(Collections.singleton(sp), w.getGrounding());
		assertEquals(spq, w.getGrounded1());
		assertEquals(Collections.singleton(spq), w.getGrounded());

		w.verify();
File
Test1.java
Developer's decision
Version 1
Kind of conflict
Method invocation