Hot answers tagged

12

There are a lot of misconceptions here. To begin, MLTT doesn't have subtypes, so Java is not going to simply be a fragment of it. It does not require dependent types to make either of the types you gave. A dependent type system doesn't need to have a "type" of types (a universe) in general (MLTT does have universes though), nor do you need dependent types ...


8

There is an (operational) semantics for Java 1.4 formulated in the $\mathbb{K}$ framework. Associated to this framework is a proof system called Matching Logic. While that page describes a prototype implementation, it seems that the functionality is being incorporated into the $\mathbb{K}$ framework tools themselves as kprover. Unfortunately, it seems the ...


7

Featherweight Java is quite highly regarded in the PL community. But if that doesn't suit your needs, here's a general approach to modelling: Formalize your language's AST into expressions and statements Write a semantics for expressions and statements. Your semantics will need: an evaluation relation, relating expression-state pairs $(e,\sigma)$ to an ...


6

Here is the question: You are given a list of length $n+1$ which contains the numbers $1,\ldots,n$, one of them appearing twice (and the rest appearing once). Find the number which appears twice. The sum of numbers from $1$ to $n$ is $\frac{n(n+1)}{2}$, so if you subtract that from the sum of the list you get the number appearing twice.


6

That of course depends on how exactly we define structured programming. We can look to the research papers that coined the phrase, such as the 1966 Structured Programming Theorem. Structured programming, as defined in these papers, would not permit partial execution of a loop body, and therefore neither a break, continue, return or throw statement (nor any ...


6

I suspect that this is intimately related to shadowing of fields in Java. When writing a derived class, I can, as in your example, write a field x that shadows the definition of x in the base class. This means that in the derived class, the original definition is no longer accessible via name x. The reason Java allows this is so that derived class ...


5

No. There's no algorithm to analyze the asymptotic complexity of a piece of code given as input. Being able to do that would tell you whether the code halted and that's undecidable.


5

The rules for traversing a tree are, to visit all nodes of a tree you do this: Preorder: (1) visit the root node, then (2) visit all the nodes in the left subtree of the root, then (3) visit all the nodes in the right subtree of the root. In steps (2) and (3), use the same rule as above. Inorder: (1) visit all the nodes in the left subtree, (2) visit the ...


4

This page on Oracle's website says: The alternative String hash function added in 7u6 has been removed from JDK 8, along with the jdk.map.althashing.threshold system property. Instead, hash bins containing a large number of colliding keys improve performance by storing their entries in a balanced tree instead of a linked list. This JDK 8 change applies ...


4

In Java, there is no 'static type of an object' - there is the type of the object, and there is the type of the reference. All Java methods are 'virtual' (to use C++ terminology), i.e. they are resolved based on the object's type. And btw. '@Override' has no effect whatsoever on the compiled code - it is just a safeguard that generates a compiler error if ...


4

Row-major order stores the rows of the array one after another in memory. That is, the array a d g j b e h k c f i l is stored as a d g j b e h k c f i l To determine the address of an element in this list, we need to know how many elements come before it. For element $[I,J]$, this is the number of complete rows above row $I$ times the length of a ...


4

I think this is due to the differences in the philosophy underlying the design of both programming languages. The C++ philosophy allows data structures to cause undefined behavior as soon as the user violates an invariant, while Java wants to avoid that in all cases. Java aims to raise exceptions when invariants are broken, or, when that can not be detected, ...


4

Here's a strategy for solving Kakuro with a SAT solver. Make a nine variables for each cell, each variable indicating whether that cell contains $1$, $2$, etc. Add a exactly-one-out-nine constraint for the variables of each cell. You can do this naively in 37 clauses by adding a clause that at least one of the nine must be true ($x_1 \vee x_2 \vee \dots \...


3

Instead of giving an answer, I will try to paraphrase the steps, I hope this will help you solve your homework. Identify the problem: What is the input? What is the output? Comprehend the problem: Can you write a formula for the problem, that relates input to the output? What is the formula for the average of x numbers? Identify different alternatives to ...


3

I recommend you look at BML. It is like JML, but for Java bytecode. It allows you to specify contracts (preconditions, postconditions, data structure invariants) at the bytecode level. I think the tools Umbra, JACK, and the Mobius program verification environment support BML, and the Mobius project is building tools that work with BML. See, e.g., the ...


3

The problem you're describing can be seen as the weighted independent set problem, as follows: Construct a graph $G=(V,E)$, where every node $v$ in $V$ corresponds to your sets of objects. The nodes $v,w$ have an edge in $E$ if and only if they share an object. The weight of each node is the number of objects contained within the corresponding set. Now, ...


3

public class Foo { public static void main(String[] java_is_silly) { System.out.print("1 2 3 4 5 6 5 4 3 2 1"); } }


3

Your approach is to try every possible $x$ and $y$ and see if $x^2+y^2=n^2$. However, $n$ is fixed and, for any $x$, either $n^2-x^2$ is a perfect square or it isn't. You can calculate what $y$ is, instead of looping and trying every possible value. Actual code is off-topic but it's confusing that you're trying to solve a problem about $...


2

"Structurally typed" means that you don't need to write implements I: if your type has all the methods I has, with compatible signatures, it's automatically a subtype of I. However, in this case, C.equals(C) does not implement I.equals(I) (due to variance) and so C isn't a subtype of I. EDIT: I'll explain: For C to be structurally equivalent to I we ...


2

You only need to use a return if you plan to return a value or object to the caller. So for instance if you called a method, that then performed a calculation such as an addition you could return the result of that calculation. If you do not need to return anything to the caller then you do not need to use a return.


2

First of all, if you want to check each combination of pure strategies, you will have two nested for loops: int a, b; for (b = 0; b < n; b++) { for (a = 0; a < m; a++) { compare(a, b); } } Additionally, compare(a,b) will then be compared to each alternative I have to exchange a under the assumption that my opponent will use b: int compare(...


2

A method is just a precise sequence of instructions (in the ordinary English-language sense of the word) of how to perform some specific task. It's certainly true that many tasks – and I mean this in a completely general sense, not just computer programs but things like recipes, travelling to work, repairing a bicycle, building a house –...


2

These are recursively defined traversal methods, as you can see from your code. A stack is useful if you want to write an implementation without recursion. Wikipedia has some explanation of the three traversals, and proposes code for the stack implementations.


2

This should really be on StackOverflow, not Computer Science, but here's an answer anyway. There are a few points. First of all, your code is not a linked list. You created an unbounded array, an array that grows dynamically (good implementations also shrink dynamically, but that is beyond the scope of this question). A linked list is defined (more or less) ...


2

Your question is equivalent to the decision version of the unbounded knapsack optimization problem. The decision is whether the maximum value (after optimization) is equal to the upper bound. Moreover, the weights and values are identical in your question (i.e. the length is both the weight and the value). Problem Formulation The unbounded knapsack ...


2

The problem is similar to coin denomination with infinite number of coins available. Let me know if this works ... http://www.geeksforgeeks.org/dynamic-programming-set-7-coin-change/ For every length which you encounter, you have two options, you can either use this rod or ignore this rod length and continue to the next one. In both the cases you can check ...


2

The Java compiler reads the files you listed with the import statements to see the definitions. For historical reasons C compiler doesn't do this and prefers to get everything in one file, hence the preprocessor. In the end, there is no magic. If you want to make sure at compiletime that the functions that you're calling exist, then the compiler has to see ...


2

I can't wrap my head around how the compiler accomplishes this. The compiler processes the source files in multiple passes. In the first pass, it gathers information about types and their members, effectively producing the information that would be contained in a header file in C++. In the second pass, it looks at method bodies and uses information from ...


2

Yes, of course. Just put all vertices in the tree into an array, in any order as you like. There are different popular methods, that all generate interesting properties: Pre-order: do a DFS starting at the root, and store the vertices in the same order as you visit them. This has the advantage, that all nodes of a subtree are next to each other. Which ...


2

Elements that are equal to the pivot are not getting moved correctly. You need to change one of your checks (> or <, pick one; usual choice is to use >=) to include the equal case in partition. Also, your else if (high_border == low_border) can just be else, since that is your only option by your while loop break condition. In that case, you do not always ...


Only top voted, non community-wiki answers of a minimum length are eligible