SE547: JIF [20/23]

Is this OK (file:Test5.jif):

  public int{Bob:} run (int{Alice:} x)
  where authority(Alice) {
    return declassify (x, {Bob:});
  }

Is this OK (file:Test6.jif):

  public int{Bob:} run (int{Alice:} x) {
    return declassify (x, {Bob:});
  }

Is this OK (file:Test7.jif):

  public int{Bob:} run (int{Alice:} x) 
  where caller(Alice) {
    return declassify (x, {Bob:});
  }